필사 모드: Rust 标准库验证行动找到的内存安全漏洞是 0 个

• 引言 — 号称史上最大规模的验证行动的结果
• 这次行动想验证什么
• 行动的结构 — 一场设有赏金的开放竞赛
• 数字 — 33,955 个函数里到底走到了哪一步
• 实际找到了什么 — 表 2 里的四行
• 该怎么读这个空结果
• 对照组 — 同一个工具，换一个代码库
  • try_fit — 1,677 万次模糊测试没跨过去的坎，20 秒跨过去了
  • 测试原理上就看不到的东西 — Firecracker
  • Cedar — 连形式化参照模型都没拦住的缺陷
• 契约打开的那扇门 — 以及一个在肯定缺陷的测试
• 当 LLM 来写规范时 — 实测的结果
• 诚实的局限 — 这些证明不保证什么
• 成本
• 那么，到底该在什么时候用，什么时候不用
• 结语
• 参考资料

引言 — 号称史上最大规模的验证行动的结果

形式化验证的故事通常是这样收尾的:"于是我们找到了一个谁都没能发现的致命漏洞。"所以这篇论文第 4.4 节的标题和开篇第一句显得有点陌生。

The verification effort has not uncovered any previously unknown memory safety vulnerabilities in the standard library.

这是 Verifying the Rust Standard Library 中的一句话，该文于 2026 年 6 月 16 日发布在 arXiv 上，并发表于 NASA Formal Methods Symposium 2026。作者名单中既有 AWS 的 Byron Cook，也混杂着 Rust 基金会、UCL、鲁汶大学(KU Leuven)、UCSD、伦敦玛丽女王大学、MIT 的研究者。用作者们自己的话说，这是"针对某个软件库所报告过的最大规模验证行动"(这是作者自己的评价)，而它的结论却是"没有新发现任何内存安全漏洞"。

这不是一个失败的故事，也不是一个成功的故事。相比宣传材料，它是一份能让我们更真实地理解形式化验证在实践中到底有什么价值的数据。本文想原原本本地把这些数字读一遍。

这次行动想验证什么

Rust 的所有权类型系统在编译期就阻止了数据竞争和相当一部分内存错误。问题在于标准库自身高度依赖 unsafe 代码。编译器不检查的五种操作 — 解引用裸指针、调用 unsafe 函数、访问可变 static、实现 unsafe trait、访问 union 字段 — 它们的健全性最终要靠开发者自己的推理来保证，而这种推理大多只记录在自然语言的 SAFETY 注释里。

论文引用的规模感是这样的:过去三年里以 I-unsound 标签报告的健全性缺陷超过 74 起，历史上已登记的 CVE 有 18 个(两个数字都截至 2026 年 3 月)。既然 Rust 现在已经用在内核、浏览器引擎、密码学库里，这次行动的动机就是想用机器检验过的证明来支撑这个基础。

这里有必要先把术语讲清楚。这次行动的目标是不存在未定义行为(UB) ，而不是完全的正确性。UB 的不存在是内存安全的充分条件，但并不能保证功能正确性、活性(liveness)或安全属性。

行动的结构 — 一场设有赏金的开放竞赛

标准库太大了，不是一个团队能验证得完的。所以它被设计成一场由 Rust 基金会运营的开放竞赛 。

验证任务被拆分成一个个称为挑战(challenge)的单元。每个挑战定义了具体的验证目标、假设列表、明确的成功标准，以及完成后支付的赏金。参与者 fork 仓库、提交 PR，技术评审委员会进行评审，通过后合并进 model-checking/verify-rust-std 这个 fork。截至论文统计口径(2026 年 3 月)，已公开 29 个挑战，收到了来自至少 4 家机构、21 名以上外部贡献者提交的 450 多个 PR。

这个数字可以直接在仓库里核实。doc/src/challenges/ 目录下从 0001-core-transmutation.md 到 0029-boxed.md 正好有 29 个文件，仓库现在仍然活跃。

这场竞赛在工具上是中立的。只要能在 Rust 标准库上运行、能接入 CI、并且能提供明确的健全性保证(通常由同行评审论文背书)，任何工具都能被接受。目前支持的工具有四个。

• Kani — 基于 CBMC 的有界模型检测。这次行动的主力。
• ESBMC — 同样是模型检测。
• Flux — 用精化类型(refinement type)检查数值范围和安全性前置条件。
• VeriFast — 分离逻辑(separation logic)。对它所覆盖的函数，能验证包括指针别名违规在内的所有 UB 都不存在。

Verus、Creusot、KRust、RAPx 这四个还在评审中。论文强调的一点是，这种多样性不是口味问题，而是必然 — 特定架构的内建函数(intrinsic)、以指针为中心的代码、并发原语、带有复杂不变式的循环，各自都需要不同的推理技巧。单一工具消化不了所有的验证条件。

数字 — 33,955 个函数里到底走到了哪一步

以 nightly-2025-10-08 工具链快照为准，core、alloc、std 这三个 crate 里一共有 33,955 个函数。

最初的 16 个月，证明都是手写的:725 个 Kani harness(其中 694 个带函数契约)，50 多个 VeriFast 证明。到 2025 年 10 月左右，新增契约的增长率开始走平。论文的诊断很冷静 — 单靠人工证明工程，从根本上就没法扩展到数万个函数。

于是他们做出了 Autoharness 。这是 Kani 内部的一个编译器 pass，会枚举一个 crate 里的所有函数、判定其资格，并在 MIR 层为每个合格的函数合成一个用完全非确定性输入调用它的证明 harness。它不改动源码 — 所以能接入 CI。

harness 有点像单元测试，但它不是用具体输入调用函数，而是用一个同时代表所有可能输入的符号值来调用。一旦模型检测器把所有可达的执行路径都毫无遗漏地探索一遍，这就不再是测试，而是一个形式化验证问题了。

函数总数                        33,955
├─ Autoharness 生成的 harness   16,748
│   ├─ 验证通过                 11,970
│   └─ 失败                      4,778   (模型缺失 / 超时 / 不支持)
└─ 跳过                         17,207
    ├─ 泛型类型参数               9,635  (56%)
    ├─ 无 Arbitrary 实现         3,826  (22%)
    ├─ Kani 内部函数              3,246  (19%)
    └─ 其他                        500  (3%)

把通过的 11,970 个函数按类别拆开是这样的:

这里论文自己加的一个提醒很重要。通过的这 11,970 个结果，分量并不都一样。

把 694 个手写契约证明也算上，用形式化函数契约验证过的函数一共是 989 个(自动 295 + 手动 694)，这是这次行动能提供的最强保证。33,955 个函数里的 989 个，大约 2.9%。

另一端是那 622 个无契约通过的 unsafe 函数。论文的解读是这样的 — 这些函数能通过，要么是(a)对 Kani 检查的那类 UB 而言明显是安全的，其 unsafe 标记是因为别名(aliasing)之类 Kani 目前还不检查的属性，要么是(b) Kani 对该函数实际行为的 UB 覆盖本身就不完整。要分辨是哪一种，需要人来看。论文把这 622 个称为不是证明，而是"自动分类挑出来的候选项"。

中间这一层最扎实。通过的 10,194 个安全函数(占 Autoharness 通过数的 85%)没有含糊之处 — Kani 对每一个被调用者(包括传递可达的 unsafe 代码)都做了符号执行，确认在所有位模式合法的输入下，没有任何一条路径会触发 UB。

实际找到了什么 — 表 2 里的四行

所以，这一切工作找到的问题，全部内容就是表 2。

四行。而其中三个根本不是代码缺陷，而是规范和文档的问题 — 缺失的安全性标注、错误的 SAFETY 注释、描述函数行为有误的文档。

论文很坦诚地把这归为一种附带收益:书写形式化规范这件事本身，就会强制人写出自然语言注释单独产生不了的、对安全性要求的精确表达。这个效果确实在 Rust 语言本身留下了痕迹 — 语言团队已经把契约(contract)接纳为一个实验性的语言特性，Rust 项目也把"给标准库标注安全性契约"定为了正式目标。

然而唯一算得上代码缺陷的第一行，"SIMD 移位结果错误"，有一个反转。论文第 7 节直接说明 — 挑战 15 是靠对 565 个 SIMD 内建函数的可执行模型做随机测试 完成的，而不是靠形式化证明完成的。为了能复现，他们记录了随机种子，也确实找到了两个上游缺陷，但用作者们自己的话说，这应该被理解为"高置信度的验证(validation)，而不是形式化验证"。

归纳一下就是这样。这场史上最大规模的验证行动在标准库里找到的那个代码缺陷，是随机测试找到的，不是形式化验证找到的。

该怎么读这个空结果

先照搬论文自己的解读。

This null result is itself informative: it speaks to the effectiveness of Rust's existing testing infrastructure and Miri-based dynamic analysis at catching memory safety bugs before they reach production.

也就是说，不要把它读成"形式化验证没用"，而要读成一个信号 — "Rust 标准库现有的测试已经非常出色了"。Miri 已经在标准库里找到了几十个缺陷，并且已经接入 CI。剩下能找到的东西本来就不多了。

接着论文重新定义了这次行动的价值。

Testing can demonstrate the absence of bugs on exercised inputs; verification certifies their absence on all inputs within scope.

测试能对已经执行过的输入证明缺陷不存在，而验证能对范围内的所有 输入证明缺陷不存在。所以这次行动真正的产出不是一份缺陷清单，而是一批常驻在 CI 里、经机器检验过的证明。每次 PR，整套工具都会针对所有生效的证明跑一遍，一旦出现违反，立刻就能被抓到。这是一道防回归的屏障。

这个说法很诚实，但冷静地看，它其实也意味着 — 这次行动的投资回报在未来。 它没有找出那些已经存在的缺陷，而是想挡住那些还没进来的缺陷，而这份价值目前还没被测量出来。

对照组 — 同一个工具，换一个代码库

如果故事到这里就结束，那结论大概会是"形式化验证对已经测试得很好的代码没什么用"。可是两周之后，2026 年 7 月 1 日，大部分同一批人又发布了 Kani: A Model Checker for Rust(目前还是预印本)。这篇论文的表 2 正好就是对照组。

Kani 在四个生产环境的 Rust 代码库里，找到了11 个 测试和模糊测试都遗漏的缺陷。

同一个工具，结果却截然相反。差别不在工具，而在目标代码现有测试的成熟度 。

try_fit — 1,677 万次模糊测试没跨过去的坎，20 秒跨过去了

这是最引人注目的案例。s2n-quic 是亚马逊对 IETF QUIC 的实现，try_fit 函数负责在给定数据包剩余容量的情况下，决定往一个 QUIC Stream 帧里塞进多少字节的数据。这是个微妙的计算，因为帧长度的变长整数编码会恰好在容量边界处变长。

s2n-quic 用的是 Bolero 属性测试框架。只要加一个 #[cfg_attr(kani, kani::proof)] 属性，同一个 harness 既能当模糊测试跑，也能当 Kani 证明跑。于是就能做这样一个对比 — 一个把实现和参照模型做差分比较的 Bolero harness，在 libfuzzer 下跑了 10 分钟以上，执行了 16,777,216 次 ，没找到失败。Kani 只用了 20 秒 就找到了一个失败的断言。

失败点就在 1 字节编码和 2 字节编码的边界附近。论文的诊断点出了要害 — 这是一片覆盖率导向的模糊测试没有梯度(gradient)可循 的稀疏输入空间，而 Kani 的符号执行会直接走到那里。

第二个 s2n-quic 案例则展示了互补性的另一面。decode_packet_number 这个缺陷，Kani 用 2.8 秒、模糊测试在一分钟内，各自独立地找到了。即便两者都找到了，Kani 给出的信息也更可执行 — 它指向的是一个具名属性的失败，而不是一次身份不明的崩溃，而且它的 concrete playback 功能会生成一个具体的反例，开发者可以把它当成一个普通的 Rust 测试重放。

测试原理上就看不到的东西 — Firecracker

Firecracker 是支撑 AWS Lambda 和 Fargate 的 VMM。它在两个安全关键组件上用了 Kani。

I/O 限流器是一个令牌桶。关心的属性是"microVM 在任意一秒的窗口内都不能超过设定的 I/O 带宽"。但这个属性本质上是依赖时间的 — 补充多少令牌取决于 auto_replenish 相对系统时钟到底是在什么时刻被调用的，这让穷举式测试变得不可能。

Kani 的解法是把 libc::clock_gettime 换成一个返回单调不减 Instant 的非确定性桩函数，把时间这个维度本身变成一个符号变量。用这个 harness 找到了限流器里的好几个缺陷，其中最重要的是一个舍入误差 — 在对抗性地精心安排调用时机的情况下，客户机最多能把自己的 I/O 预算超出 0.01%。

这里得说句老实话。0.01% 在实务上是个很小的超出量。要是把它包装成"致命漏洞"，那就是在撒谎。有意思的不是它的量级，而是它的种类 — 这个误差取决于补充调用相对系统时钟究竟发生在亚毫秒级的哪个精确时刻，而这正是测试没法确定性地控制、模糊测试在没有显式时间模型的情况下也瞄不准的一类条件。

第二个是 VirtIO 设备仿真。主机和客户机共享的内存是一个对抗性的攻击面 — 不受信任的客户机可以往共享的描述符和环形缓冲区里写入任意值。Kani 用非确定性的客户机内存来表示这个场景，验证了对 VirtIO 规范 2.6.7.2 节的合规性，还额外找到一个缺陷:客户机可以把一个 VirtIO 队列组件的起始地址放进 MMIO 空隙，让 Firecracker 在启动过程中 panic。

Cedar — 连形式化参照模型都没拦住的缺陷

Cedar 是一个开源的授权策略语言兼引擎。这个案例特别的地方在于，Cedar 本来就已经在对一个形式化参照模型做差分测试 。即便如此，缺陷还是活着进了生产代码。

contains_at_least_two 检查一个字符串里某个子串是否出现了两次以上。如果把一个多字节字符当作查询词传进去，就可能在非字符边界处切开 &str，引发运行时 panic。所有现有测试都对此保持沉默。Kani 的符号执行生成了一个反例，修复以 cedar PR 1037 的形式合并(2024 年 7 月)。

留意一下日期。Kani 论文是 2026 年的，但每个案例本身的年份并不统一 — Cedar 的修复是 2024 年的事。论文是在 2026 年把这些案例汇总报告出来的，并不是说这 11 个缺陷全都是在 2026 年发现的。

契约打开的那扇门 — 以及一个在肯定缺陷的测试

Hifitime 是一个高精度时间管理库，用在了 Firefly 的 Blue Ghost Mission 1 号月球着陆任务里。这里是 Kani 论文的契约(contract)案例研究。

Kani 的契约用 Rust 布尔表达式来写函数的前置条件、后置条件和循环不变式。这为什么重要 — 因为它把有界模型检测提升到了无界 保证的层次:不是穷举式地展开循环，而是验证不变式具有归纳性，然后用它来抽象掉循环。用论文的说法，第一阶段证明一个操作不会崩溃，第二阶段证明这个操作计算正确 。

作为确立功能属性的一个副产品，Kani 找到了 6 个此前未知的缺陷 — 这些属性是仅有"不发生 panic"的 harness 根本表达不出来的。其中最有意义的两个，违反的是 Rust 标准库自身的要求。

• Epoch 的 PartialEq/Ord 不一致。 Duration::PartialEq 故意把符号相反的值视为相等(因为它表示的是一段与方向无关的区间长度)。可是 Epoch::PartialEq 委托给了这个实现，而 Epoch::Ord 用的却是区分符号的字典序比较。Rust 标准库要求如果 a == b，那么 a.cmp(b) 必须是 Ordering::Equal。在所有符号相反的 epoch 对上，这个不变式都被打破了。
• Duration 的 PartialEq/Ord 不一致(过零点)。 同样的根源。两个 Duration 可以同时满足 a == b 和 a < b。

Epoch 这个缺陷为什么没被测试抓到，把这篇文章的要点浓缩成了一句话 — 因为没有任何测试拿一个 epoch 去和它符号翻转后的版本做比较 。这对"时间点"来说是个概念上很奇怪的操作。Kani 的符号执行在遍历所有可能的 Epoch 对时，自动生成了这个输入。

还有最扎心的一个细节。当契约抓到 total_nanoseconds() 的一个符号错误(在负方向超过一个世纪的时长上，用了减法而不是加法)时，修复只是源码里的一个字符。可是有一个现成的集成测试正把那个有缺陷的行为断言为正确的 ，必须和实现一起修改。论文的诊断很尖锐 — 因为那个测试的判定标准(oracle)本来就是照着实现的输出写的，所以它把同一个错误原封不动地编码了进去。相比之下，后置条件是从 Duration 类型的编码不变式推导出来的，所以能独立地检查实现和测试双方。

这个陷阱在论文之外也能得到印证。Hifitime 仓库的 issue 475 是在 Kani 验证工作(PR 474，2026 年 4 月合并)期间发现的 try_truncated_nanoseconds 错误分类缺陷，issue 正文这样写道 — "为了让证明通过，把 Kani harness 更新成匹配当前(错误)的行为;实际实现还需要单独修复。"把规范凑成实现的样子，验证就能通过，缺陷却留了下来。就算手里有验证工具，规范到底从哪里来，人依然说了算。

当 LLM 来写规范时 — 实测的结果

Hifitime 的第二阶段规范是用一个有 shell 访问权限的 AI 编程助手开发出来的。工作流是一个很紧的循环 — 助手提出一个契约标注，写进源码，跑一次 cargo kani，观察结果(成功/失败/超时/编译错误)，再打磨规范。人类研究者负责指定该瞄准哪些函数、提供领域背景，并审查所提议契约的合理性。

Kani 的规范语言是 Rust 的一个扩展，这一点在这里帮了大忙。因为契约就是 Rust 布尔表达式，harness 就是 Rust 函数，所以助手不用去学一门单独的形式化语言，直接用已有的 Rust 知识就够了。

论文强调的是结构，而不是结果本身。

Crucially, the specifications do not need to be trusted: Kani verifies every contract against the implementation.

意思是规范不需要被信任。事实上，AI 生成的 3 个契约验证失败了，Kani 三个都抓住了。

1. 一个背不动的后置条件，在自己的 ensures 子句里调用了正在被验证的函数本身 — SAT 公式翻了一倍，求解器超时。(助手把它简化成了一个直接的算术表达式)
2. 一个过宽的符号输入(kani::any::<Epoch>())把 TimeScale::ET 这个变体也带了进来，连带把 sin() 也拖进了 SAT 公式，导致超时。(限制为 TimeScale::TAI)
3. 一个 const fn 不兼容问题 — Kani 的宏展开生成了非 const 代码，导致编译错误。(改用一个独立的证明 harness)

分类一下:一个规范设计错误，一个 harness 设计错误，一个 Kani 自身的限制。三个都是助手仅凭 Kani 的输出，在同一个会话里诊断并修复的。

这是 LLM 证明自动化的故事里少见的诚实的一面 — 值得吹嘘的不是"AI 把规范写得很好"，而是"AI 把规范写错了，验证器也能把它筛出来"。核心在于 Kani 抓住了人类审查可能会漏掉的东西(用论文自己的话说，"all caught by Kani, not human review")。

与此同时，标准库这边的 LLM 实验要谨慎得多。他们尝试了基于 LLM 的契约合成，把自然语言的 SAFETY 注释翻译成函数契约，但论文把这称为"初步的(preliminary)"，指出生成的契约在合并前需要人工审查，并把精确率和召回率的系统性评估留给了未来的工作。这方面目前还没有发表可以引用的数字。

诚实的局限 — 这些证明不保证什么

NFM 论文第 7 节的标题是"Limitations and threats to validity"，写得比一般形式化验证的宣传材料密实得多。值得原样搬过来。

有界推理。 Kani 默认是有界模型检测 — 把循环展开到一个设定的上限为止。如果上限不够，展开断言(unwinding assertion)就会失败，证明会被报告为失败，所以不会悄无声息地出错。但它不验证终止性 ，因为 Kani 目前还不支持循环变量(decreases)子句。

部分的属性覆盖。 Kani 只检查 Rust 参考手册所列 UB 中的一个子集。它不 检查的东西相当可观。

• 违反指针别名模型(Stacked Borrows / Tree Borrows)
• 数据竞争
• 错误的内联汇编
• 部分与来源(provenance)相关的 UB 形式
• 跨越 unsafe 边界的类型安全不变式的保持(例如 Vec 的长度不超过其容量)

照论文原文的说法 — 一个通过了当前所有检查的函数，在一个更完整的模型下仍然可能表现出 UB。

规范与模型之间的空白。 Rust 目前还没有一份被批准的形式化规范 。像别名模型这样的核心部分存在相互竞争的提案，未来规范一旦变化，今天在这些假设下健全的证明就可能失效。对调用了内建函数或外部函数的函数所做的验证，取决于给这些操作提供的模型有多忠实，模型不准确就可能产生不健全的验证结果。

工具链的健全性。 所有结果都依赖于工具本身的正确性 — Kani 的 MIR-to-GOTO 转换、CBMC、被调用的 SAT/SMT 求解器、VeriFast 的符号执行引擎。论文直接写明:这些工具没有一个自身是经过形式化验证的。 它们的可靠性靠的是大量的测试与模糊测试，以及多年的生产环境使用。

并发完全是空白。 29 个挑战里有两个瞄准并发 API — 挑战 7(atomic 类型)和挑战 27(Arc)。两个都没有一份被批准的解答 ，尽管 unsafe Rust 里的数据竞争本身就是即时的 UB。难的地方在于:在弱化的内存模型下，为无锁数据结构写规范并验证它们。

剩下的地盘。 验证过的函数超过一万个，但标准库离完全验证还差得远。BTreeMap 的内部实现、atomic 类型、String、迭代器、向量、双端队列、引用计数类型等一大批影响力很大的 API，要么只被部分覆盖，要么根本还没碰过。

Kani 论文也承认了自己案例研究里的偏差 — 被评估的项目不是随机样本，而是自己主动采用了 Kani 的地方 ，有利的案例可能因此被过度代表。论文写道，Cedar 那次实验是对一个原本没在用 Kani 的项目做的有意评估，这在一定程度上缓解了这个问题。

成本

证明的维护。 验证仓库是上游 rust-lang/rust 的一个 fork，需要定期同步。可 Rust 每六周就发一个新版本 。论文的结论是，要让这套方式可持续，契约和证明就必须被搬到上游去，让证明维护成为标准开发流程的一部分。现在还不是这样。

编译时间。 随着 harness 数量暴涨，编译成了瓶颈。他们做了一个专门的编译器基准测试工具，加入了并行化、缓存、启发式的代码生成顺序、函数打桩(stubbing)，让标准库的编译获得了 3.97 倍的速度提升(作者自测，相对于一个朴素的顺序流水线)。

CI 时间。 以 Kani 论文的表 1 为准。

大多数在 25 分钟内就能跑完。论文的说法是，这是一个能塞进 PR 工作流的预算，看这张表也确实说得通。不过表里也能看出 harness 数量和时间并不是线性关系 — 只有 1 个 harness 的 rust-sel4 要 4 分钟，有 10 个的 zerocopy 反而只要 3 分钟。比起 harness 的数量，单个证明的难度才是主导因素。

人和组织的成本。 论文第 5.1 节是最坦率的部分。它承认最初的计划专注于技术里程碑，严重低估了 社区共识和机构协调所需的时间。要把契约整合进 Rust 编译器，需要语言团队、库维护者、工具作者的广泛支持，哪怕是技术上很简单的改动，只要没有及早把利益相关方拉进来，也会卡住。和外部机构的合作需要耗时数月的法律协议 。要吸引外部贡献者，光靠赏金也不够，还需要有难度梯度、清晰的文档、能跑起来的示例。

按工具计的开销。 用 VeriFast 证明 LinkedList 的 PR 238(挑战 5，2025 年 8 月合并)很好地展示了这种成本。它直接验证了 19 个函数，并蕴含了另外 5 个函数的健全性，但 VeriFast 要求对源码做一些小的改写来插入 ghost 指令(例如把 for 循环改成 loop，把 Option::map 改成它的一阶等价形式)。所以 CI 流水线分三个阶段 — VeriFast 检查带注释的代码，一个精化检查器(refinement checker) 用机器的方式验证原始代码的每一种行为也都是注释版本的行为，再用 diff 确认原始代码和上游一致。这清楚地展示了演绎式验证相对模型检测多出来的工程负担，同时也是换取那份更深保证(所有 UB 都不存在)所付出的代价。

那么，到底该在什么时候用，什么时候不用

把两篇论文叠在一起看，判断标准就相当清晰了。

值回成本的情况

• 存在一种既有测试原理上够不着的属性。 依赖时间的代码(Firecracker 的限流器)、面对敌对输入的共享内存边界(VirtIO)、像编码边界这样的稀疏输入区域(try_fit)。模糊测试没有梯度的地方，正是符号执行该出场的地方。
• 代码范围窄，状态空间明确。 表 1 里那些 CI 时间短的项目的共同点。
• 属性可以写成规范。 像 Eq/Ord 一致性、编码-解码互逆这样、能独立于实现推导出来的不变式存在时，契约才能发挥真正的价值。Hifitime 的案例说明了这一点。
• 目的是防止回归。 哪怕代码已经测试得很好，一个常驻在 CI 里、经机器检验的证明也能抓住未来的回归。标准库这次行动真正发挥作用的地方就在这里。
• 已经有属性测试了。 像 s2n-quic 用 Bolero 那样，只需一个属性，同一个 harness 就变成了证明。边际成本几乎为零。

过度或者时机还没到的情况

• 代码已经达到了 Miri 级别的验证程度。 标准库的结果正是这种情况。抱着找新缺陷的期待进去，只会失望。
• 泛型是代码的核心。 Autoharness 跳过的函数里有 56% 是泛型的。因为 Rust 在编译期做单态化，没法为未实例化的类型参数合成输入。
• 并发是核心问题。 挑战 7 和 27 没有一份被批准的解答，这个事实本身就说明了当前的成熟度。弱化内存模型下的无锁数据结构，依然是个悬而未决的问题。
• 别名、数据竞争是主要风险。 Kani 不看这些。这块地盘依然归 Miri 管。
• 打算把规范从实现里抄过来。 就像 issue 475 和上面那个 Hifitime 缺陷所展示的，照着实现写出来的规范，会把实现的缺陷原样编码进去。这样一来验证能通过，缺陷却留了下来。没有一份能独立推导出来的规范，验证就是一种昂贵的同义反复。

浓缩成一句话就是:形式化验证的价值，不是和工具有多强大成正比，而是和你现有测试够不着的地盘有多大成正比。

结语

这两篇论文需要放在一起读，原因就在这里。只读一篇，就会得出错误的结论。

只读 NFM 那篇，结论会是"史上最大规模的验证行动找到了 0 个缺陷 — 形式化验证被过度炒作了"。只读 Kani 那篇，结论会是"1,677 万次模糊测试都没找到的东西，20 秒就找到了 — 为什么现在还没人用"。两者都是同一个工具、同一支团队的结果。

真正的结论就在两者之间。标准库里没冒出缺陷，不是因为工具弱，而是因为目标代码已经被多年的 Miri 和测试打磨过了;s2n-quic 和 Hifitime 里冒出了缺陷，也不是因为工具有魔法，而是因为那些代码里存在测试原理上够不着的角落。形式化验证不是测试的更高版本，而是一张形状不同、和测试互补的网 。

最后，这次行动留下的最大资产，或许根本不是那 11,970 个证明。契约成了 Rust 的一个实验性语言特性，给标准库标注安全性契约也成了项目的正式目标。原本只写在自然语言 SAFETY 注释里的东西，开始转移成机器可读的形式 — 在这个空结果背后悄悄发生的这场变化，大概才是走得更远的那部分。

参考资料

• Verifying the Rust Standard Library (Cook 等，NASA Formal Methods Symposium 2026，arXiv 2606.17374) — 这次行动的成果论文。DOI 10.1007/978-3-032-28079-4_19
• Kani: A Model Checker for Rust (arXiv 2607.01504，2026 年 7 月 1 日预印本) — 工具论文。工业代码库案例研究与 11 个缺陷
• model-checking/verify-rust-std — 验证仓库 — 29 个挑战可以在 doc/src/challenges/ 下直接查到
• verify-rust-std PR 238 — VeriFast 对 LinkedList 的证明(挑战 5)
• Kani Rust Verifier — 工具仓库
• cedar PR 1037 — 修复 contains_at_least_two 里潜伏的缺陷
• hifitime issue 475 — 在 Kani 验证过程中发现，把 harness 迁就成缺陷行为的一个案例
• Kani 检查的未定义行为清单 — 用来确认它不检查什么