Anthropic 报告，Claude 为 123 个开源库的 239 个 OSS-Fuzz 入口点生成了形式化证明，证明对象落到编译后的 RISC-V 二进制。这个结果足以改变证明生产的成本结构，却无法直接回答国内技术负责人在上线会上最关心的问题：我们正在部署的这套 x86 或 ARM 服务，能继承多少证明结论？
解决这个问题不需要先审阅约 1.8 亿行 Rocq 证明。更有效的做法，是要求提交方带来三张表：证明命题表、工件映射表和残余风险表。三张表共同构成一份面向部署的证明覆盖合同。这里的证明覆盖指上线保障清单，范围大于形式化工具中用于检查空证明、依赖关系或结构遗漏的单一 coverage 指标。
第一张表：proof checker 究竟通过了什么
把 formally verified 拆成可以逐项询问的字段：
| 审查字段 | 本次研究中的答案 | 容易被误写成什么 |
|---|---|---|
| 证明对象 | 特定编译配置产生的静态 riscv64 二进制 | 整个源代码仓库 |
| 入口面 | 选定 OSS-Fuzz harness 可到达的路径 | 库的所有 API 和调用序列 |
| 输入域 | 研究主文使用小于 64 MiB 的 driver 边界；公开 statement 量化 LPS-valid 进程输入 | 任意现实流量与资源条件 |
| 性质 | 不触发模型中的 fault、abort、未建模行为，并对特定普通版与 sanitizer 版建立可观察行为关系 | 功能、性能和安全全部正确 |
| 命题前提 | 每条 statement 的内存预算、系统调用失败策略、初始状态、调用者和外部干扰条件 | checker 通过后无需再满足环境条件 |
| 执行模型 | 单线程、静态链接、RISC-V、musl 与固定版本 LPS；模型范围和精度缺口另行披露 | 常见 x86/ARM、glibc、多线程服务 |
| 可信基础 | 定理、Rocq kernel、允许的公理、RISC-V/Linux 模型和二进制转模型工具 | 证明本身无需信任任何组件 |
Anthropic 的技术附录把研究命题中的 no-crash 进一步限定为：没有 fault、abort 或未建模行为。普通版与插桩版还需在标准输入输出、退出方式和最终文件系统状态等观测量上保持一致。公开仓库中的正式 statement 还绑定普通版内存预算前件与允许的系统调用失败方式，必须逐条读取。行为一致性没有覆盖性能，也不能自然排除静默死循环，除非另有终止性命题。
因此，会上看到 proof checker 通过时，正确结论是定理成立。下一步仍要检查定理是否表达了团队真正想关闭的风险。
第二张表：证明工件与上线工件是否是同一个对象
Theorem Labs 公开的 oss-verify-proofs 仓库提供了一个可操作样板。当前公开版本是研究结果的子集，包含 25 个库、60 个入口点。按 statement 统计，仓库列出 20,164 条命题，其中 138 条已证明，且当前公开证明没有 halts statement。入口点数量因此不能充当性质完整度。仓库同时记录 Rocq 9.2.0、checker 镜像摘要、Linux Process Semantics 提交、编译器与 sanitizer 版本、上游提交、二进制 SHA-256 和允许的公理。
这组记录说明，形式化证明也需要供应链身份。上线工单至少应绑定：
- 上游源码提交与构建配方；
- 编译器、链接器、libc、sanitizer 和参数；
- 被证明二进制的 SHA-256；
- 定理标识、入口点、输入和内存边界；
- 模型、checker 与容器镜像版本；
- 实际部署架构、动态链接、并发模式和调用者前置条件；
- 公开与未建模行为、假设负责人、验证方法和当前状态；
- proof hash、checker 输出、允许公理报告、CI 日期和独立复跑状态；
- 证明工件到生产工件的差异矩阵、补偿控制与重证触发器。
这里的工件也不总是最终二进制。CompCert 的正式证明边界位于完成预处理、解析和类型处理后的 C AST，与装配和链接前的 Asm AST 之间。通用合同应记录被证明的表示层和变换边界；在 Anthropic 这个案例中，该表示层才是精确二进制字节。
逐项比对后，评审会落到三种处置分支。
完全匹配。 生产直接使用同一个被证明工件，并满足模型假设。证明可以作为该命题的上线门禁。
存在可证明的桥。 例如另有经过审查的等价性证明，能够连接被证明工件与生产工件。团队应把桥的定理和可信基础一起纳入发布记录。
只有组件级证据。 现实中最常见：生产使用 x86-64 或 ARM、glibc、动态链接、多线程和更大的应用调用图。这时保留证明的价值，但它只能降低特定入口与性质的风险。未覆盖部分继续依赖测试、Fuzz、代码审查、灰度和运行时监控。
工件、定理、命题前提、模型、checker、调用方式或部署环境任何一项发生变化，证明就从当前证据退化为历史证据，直到重新核对、重新证明或补齐等价桥。
第三张表：哪些风险仍然开放
Anthropic 主动列出了最容易被宣传语遮住的边界。
首先，sanitizer 能检测的错误集合小于全部错误集合。返回错误结果、权限逻辑缺陷、资源泄漏或某些内存问题，可能完全不触发 no-crash 命题。
其次，入口点决定可达范围。一个 harness 的全输入证明，只覆盖从这个入口可到达的代码。Dead code、其他公共函数、复杂调用序列和调用者误用仍然开放。即使所有现有 fuzz 入口都通过，也不能自然推出整库正确。
再次，形式化机器模型与现实机器之间存在语义差异。研究针对单线程静态 RISC-V 与 musl；主流生产环境通常选择另一套 ISA、libc、链接方式和并发模型。固定版本 LPS 官方标注为 best effort、incomplete，并列出未检查假设与已知精度缺口。在部分缺口中，行为集合的等价关系可能在 LPS 内成立，却在受支持的真实系统上不成立。模型中没有描述或描述不精确的行为，不能靠 proof checker 自动消除。
最后，自动修补后继续证明会引入目标投机风险。Claude 可以删除功能或收窄行为，让定理更容易成立。Anthropic 为此惩罚补丁、鼓励证明行为变化并保留审计记录。生产流程应把两个门禁分开：
- 证明门禁回答补丁后的二进制是否满足定理；
- 行为门禁回答补丁是否只改变预期行为，是否通过 Diff 审查、回归测试、兼容性检查和必要的等价性验证。
证明通过不能替代行为变更审批。
这项研究真正改变了什么
Anthropic 报告，典型证明约 60 万行，而被证明二进制的中位长度约 1.8 万条 RISC-V 指令。人类逐行审证明已经没有经济意义，审查重点转移到短得多的定理、模型、构建来源与可信基础。
证明过程还发现了传统 Fuzz 很难触达的错误，例如需要罕见的大输入布局、跨句柄调用序列或深层嵌套才能出现的问题。这说明证明不仅是最终证书，也是一种缺陷发现方法。
规模化成本仍然很高。附录称单个证明的 checker 运行可能需要 30 分钟到数小时 CPU 时间；研究主文还指出证明生成可能消耗数亿 Token。共享既有证明后，36 个小任务的 Agent 平均少用 17% Token，说明复用公共运行时、内存模型和库证明是后续降本路径。
这些数据支持的结论是：LLM 已经显著扩大自动生成并机器检查证明的范围。它们暂时无法支持另一个更强结论，即形式化验证已经可以无差别替代生产软件的安全测试。
把证明覆盖合同接入现有上线流程
对没有形式化方法团队的组织，可以从一个高风险解析器或解码器开始：
- 选择攻击面清晰、已有 Fuzz harness 的入口；
- 让维护者确认不可信输入、最大尺寸、预期失败和必须保持的性质；
- 将每条性质写成能够真实失败的检查，并用 seed corpus 与 mutant 验证它并非空命题；
- 固定构建配方与二进制哈希，逐条记录命题前提、模型版本和独立 proof check；
- 填完三张表，把未覆盖风险分配回测试、审查和运行时控制；
- 只有证明工件、命题前提与上线环境匹配，或存在可信等价桥时，才关闭对应的有界发布风险；
- 为工件、依赖、构建、模型、调用者或环境变化设置失效与重证规则。
形式化验证的价值来自结论精确。运营流程也应该保持同样精确：证明了哪个对象、哪个性质、哪个范围，就关闭哪个风险。其余风险继续开放、继续有负责人、继续有证据要求。