从测试套件到验证系统

我们跨过的那条线

测试套件断言你想到要检查的行为。它靠叠加生长：发现一个缺口，写一个测试，感觉更好。它隐蔽的失败模式是：它测量的是努力，不是对风险的覆盖 — 而且它无法告诉你它从未见过的东西。

验证系统多做出四个声明，每一个都是机制，不是感觉：

1. 每条声明都绑定证据 — 双向绑定，没有孤儿测试，也没有无证据的声明。
2. 证据是版本化的 — “92/92 覆盖”毫无意义，如果不说明对哪个 corpus、哪个编译器、哪个 revision。
3. 检查者本身被检查 — 验证你语言的那件工具，本身就是安全关键工件。
4. 证据有层级 — “测过”、“机械分析过”和“机器检查的证明”强度不同，而打包方式要让这个差别清晰可读。

两周前我们只部分拥有 (1) — 一个 92 条手动声明的 claims 台账和一个 lint gate。(2)、(3)、(4) 我们都没有。这篇文章讲的是构建它们教给我们的东西。

重新定义问题的那次调研

我们从你该开始的地方开始：那些真正做认证的人怎么做？阅读清单是 CompCert、DO-330、Csmith、Rust 的 Crater、Alive2 和 SPARK — 令人惭愧的是，这里面关于“多写测试”的部分少得可怜。

CompCert 携带一个机器检查的证明：它的输出实现了它的源语义 — 而且在 2026 年 3 月，它成为第一个拿到 DO-178C/DO-333/DO-330 认证 credits 的编译器。教训不是“去写证明”（我们写不起；成本随语言规模增长）。教训是：认证机构接受分层的证据 — 有证明的地方给 proof credits，没有的地方给基于需求的测试，按 objective 打包。

Alive2 展示了实用的中间路线：translation validation，每天跑在 LLVM 自己的测试套件上，带一个公开的 bug 台账。对优化做自动验证并给出反例 — 不需要证明编译器本身。

Csmith 用一个方法在每个量产 C 编译器里都找到了 bug：数百万个随机生成的无 UB 程序，配一个 differential oracle。CsmithEdge 接着记录了天花板：靠限制程序形状达到正确的生成器，会偏向惯用写法，恰好藏住那些边界 bug。记住这句话；文末它会回来。

Rust 的 Crater 每周发布编译器而没有静默回归，方法是在工具链 N 和 N+1 下构建整个生态并做 diff。SPARK 重新定义了语言本身：设计成重要的声明可证明 — “无运行时错误”作为交付物出厂。

DO-330 是意外。它根本不是关于测试你的软件 — 它是关于合格鉴定你所使用的工具：要求对工具有基于需求的测试，在工具自己的测试运行中做结构覆盖，以及双向可追溯性、不可追溯的测试一律删除。如果你的编译器是你安全论证的一部分，那编译器就是安全关键工件，要像安全关键工件一样被审计。

我们带回了七条排序后的采纳项。以下是每一件教给我们的东西。

七件仪器

1. 构建 profile 间的字节一致性

教条早就写了“profile 即语义” — 同一套件必须在 --release 和 --debug 下都通过。但我们的 profile sweep 只比较通过/失败。一个改变了打印输出却让测试保持绿色的 miscompile — 一个浮点数渲染得不一样、一个求值顺序被翻转 — 会通过。GCC torture-test 的实践更严格：同一份源码，所有优化级别，字节可比较的行为。我们的 parity gate 现在要求 97 个套件在三个 profile 下 transcript 逐字节一致。任何 diff 按构造就是一个优化增量里的 miscompile。

教训：通过/失败的契约只能看见测试已经断言的失败。字节一致性看见程序打印的一切。

2. 跨编译器版本的回归网

这次战役里，SDK 有三次在我们脚下悄无声息地移动了，每次都是不同的仪器迟到了才发现。Rust 用 Crater 解决这个问题；我们的同一想法的版本，对 152 份已提交的 per-suite transcript 跨 SDK 版本做 diff，并对 verdict 翻转设 gate：一个测试从 ok→FAILED 是回归候选，FAILED→ok 是一个必须引用其 ticket 的修复，而每一个未分类的变更都让整个 run 失败。一个 annotations 台账承载这些理由。

它第一次真跑就发现 29 份 transcript 从未被提交 — 两个 corpus 包有本地 ignore 规则，悄悄把它们排除在版本固定的证据之外。回归网只和它覆盖的东西一样好，而它在第一天就审计了它自己。

3. 对工具本身做合格鉴定

没有任何东西测量 corpus 练习了编译器的哪些部分。对发布编译器做语句级覆盖被证明是不可能的 — 它是自托管的，而对你正在认证的工件做插桩，就改变了这个工件 — 所以我们构建了 DO-330 的诚实等价物：对工具的需求表面做覆盖。--help 里的每个 flag 和子命令（59 个表面）必须被 corpus 工具练习到，或者带一份书面理由。每个 warning 通道必须听令而响 — 用效果验证，不是用 flag 接受来验证。还有一类我们曾忽略的新信号：IR 多样性。一个只被一个 corpus 文件发出的 LLVM opcode，是一条零冗余的 codegen 路径；三个被 pin 住了，现在出现新的一条会让报告失败。

这个通道立刻挣回了身价：一个 retained-memory 警告被发现在其手册记录的任何形状上都不响，一个 violation 诊断把标准库自己的 print 调用标成了 package-private。两者都已作为 ticket 报给上游。

教训：认证的本能 — 审计工具，而不只是工件 — 在教科书式的插桩不可用时，依然能找到真实缺陷。

4. 数量，以及限制的代价

我们的 metamorphic fuzzer 每个 run 跑 60 个程序。Csmith 的方法是数量 — 多年里数百万个程序 — 于是我们扩到每个 run 1,000+，带逐程序 seed pinning、任何 divergence 的自动约简（CReduce 风格）、以及一个给发现去重的 fingerprint 台账。一千个程序现在花 6.6 分钟，全绿。

然后 CsmithEdge 的警告在我们自己家里应验了。我们的安全语法只由验证为绿的格子构成 — 按构造正确，也按构造失明。complement 生成器把 escape-analysis 网格枚举的边界家族组合起来 — hoisted scratch 数组、factory drop、参数存储 — 并用 analyzer 契约本身当 oracle：dump verdict 必须有 witness 背书，运行时内存增长必须与 verdict 一致。

5. 双通道证据，或者：我们自己的工具如何抓住我们自己的工具

这是整篇文章都值得的那个故事。edge-grammar fuzzer 的第一天暗示：我们追踪了几周的泄漏家族已经修复了 — 100k 和 1M 迭代下运行时内存持平。我们差点把它记成一场胜利。

store-grid 重建说了不然。我们给每个 pin 住的家族两条腿：已有的 dump 腿（analyzer 声称什么）和一条新的 runtime 腿（内存做什么）。真正的 hoisted scratch 数组形状以 16 B/iter 泄漏，dump 与 runtime 一致。fuzzer 的“已修复”读数是个伪影 — 它的生成器一直把 scratch 数组分配在循环内部，那个天真的总是释放的形态，而不是文档记录的模式。

于是我们自己公布了更正：“该泄漏没有修复；我们的测量是伪影；这是生成器的 bug。”而更正后的图景真的有用：另外三个被追踪的家族，泄漏的一半确实修好了（dead store 在 codegen 被消除），而 analyzer 仍然宣称没有 witness 的 definite — 也就是说每个 ticket 都裂成修复了的泄漏半边和未解决的定级半边，这是另一个缺陷类别，需要另一种修法。

教训：一个测量通道是一种意见。两条必须一致的独立通道，把分歧变成发现，把伪影变成更正。网格逼我们在别人之前 retract 了自己。

6. 每个契约的两个方向

一个 warning 通道不被一个能触发它的形状验证。它由一个能触发它的形状加上旁边必须保持沉默的正确代码验证。warning 网格在每个 warning 通道上 pin 了 11 个 trigger 格子和 10 个 silence 格子 — 而找到那个 false positive 的正是 silence 格子。开发期间，vacuous-match 守卫抓到两个格子因错误的原因通过（一个空 flag 让每个匹配平凡为真）。一个不会失败的 checker 不是 checker；这一个现在可证明地双向失败。

7. 打包：binder 与 stamp

DO-330 的洞见是：认证在多大程度上是打包，就在多大程度上是测量。最后两块：

qualification binder：20 个 objective，每个映射到带显式层级的证据 — PROOF（机器检查）、ANALYSIS（对工件的机械仪器）、TEST（执行过的断言）。一页纸回答“什么被证明、被分析、被测试”，而一个证据没有跑过的 objective 渲染为红色 — 没跑的 gate 价值为零。

provenance stamp：每份报告现在携带 {plan revision × SDK 版本 × corpus hash × git rev}，确定性且字段隔离。没有 stamp 的报告不是证据，未版本化的声明同样不是。回归 diff 消费这个 stamp 来在 SDK 升级间自动配对快照。

教训，直白地说

“生产可用”分解为证据，而证据分解为层级。测试展示你想到了的 bug 的缺席。分析机械化地扩展覆盖。证明完全关闭一个域。三者互不包含；一个不说每条声明由哪个层级背书的认证，是把混合物当纯度卖。

工具是表面的一部分。warning 网格和表面覆盖仪器找到的每个缺陷都是编译器缺陷，不是 corpus 缺口。团队鉴定他们的测试套件，却从不审计消费它们的编译器 — DO-330 的存在就是因为这个本能是反的。

限制有价格，而且你在看不见的地方支付它。每个安全语法同时也是一个盲区。CsmithEdge 警告过；四天后我们自己的 fuzzer 证明了它 — 因为论文预测的那个原因，误读了一个被追踪泄漏家族的状态。要故意构建那个互补的、不安全的生成器，配一个不同的 oracle。

一个通道是一种意见。dump verdict 和运行时内存是独立的证人。它们一致的地方，你有一个事实。它们分歧的地方，你有一个发现 — 而分歧的类别告诉你它是什么种类：claim 与 codegen 的不一致比不精确更糟。

更正是一种能力。这个双周里我们的仪器做的最好的事，是逼我们在任何其他人之前公开 retract 了我们自己的结果。一个不能让作者难堪的验证系统不是在测量。

沉默必须被测试。我们找到的每个 false positive 都是一个缺失的 silence 契约。只有 trigger 的测试，在又聋（漏掉真触发）又吵（对正确代码狼来了）的通道上夸大信心。

而诚实的边界仍在。没有插桩构建，编译器的语句级覆盖仍然不可能。大 SDK 包上的形状深度仍然是最弱的一层。formal kernel 覆盖数值域和内存生命周期，不是整个语言。认证是一道楼梯，而你能陈述的边界，比一个只能盼望的天花板更值钱。

我们会告诉一个明天起步的团队什么

1. 盘点你的声明，把每条双向绑到证据上，用 gate 强制，而不是靠约定。
2. 给每个工件盖上 {什么，对什么，何时} 的章，否则接受它们没有一样是证据。
3. 加一条你不控制的 differential 通道（另一个编译器、另一个 profile、另一个版本）— 它比再一千个自洽的测试更值钱。
4. 如果可以，给每个 pin 住的期望两条腿 — 一条声明和一条后果 — 并把分歧当作你拥有的最有价值的信号。
5. 审计工具。然后审计审计。两者都会找到东西。

完整的调研与来源、仪器契约、以及每个 objective 背后的验收证据，都随项目的验证工具一起存放。楼梯还在继续。