Claude 为百余开源库生成正确性证明

Claude 生成了约 1.8 亿行证明代码，还在验证过程中发现数百个常规测试遗漏的 bug。但这次实验验证的是已有软件，并不能直接推出「AI 写出的代码已经安全」。

Anthropic 与 Theorem 想做的，是让 AI 承担昂贵的数学证明工作，再由独立程序检查证明是否成立。对程序员来说，值得关注的不只是发现了多少漏洞，还有这些证明覆盖了什么，以及它离日常开发还有多远。

1.8 亿行证明，究竟证明了什么

形式化验证（formal verification）要用数学方法，证明程序在指定条件下满足某些要求。测试检查选中的输入会发生什么，形式化验证则尝试覆盖条件范围内的所有情况。

这件事过去很贵。原文举例，专家团队为小型操作系统内核 seL4 完成形式化验证，投入了 20 人年，因此它通常用于 Airbus 航空电子软件这类高要求场景。

这次，Anthropic 的 Frontier Red Team 与 Theorem 合作，从 Google 的 OSS-Fuzz 安全项目中取用涉及 123 个开源库的测试程序。Claude 把崩溃测试转化为数学问题，分析编译后的机器码，并在几周内生成约 1.8 亿行证明代码。

这里有两个容易误读的地方：1.8 亿行是证明代码，不是新增的业务代码；涉及 123 个库的测试程序，也不能理解成已经完整证明了这 123 个库的全部行为。

证明交给独立验证程序 Rocq 自动检查。按 Anthropic 的说法，这个过程几乎不需要人工审查。研究人员称其为「完全自主」生成证明，不过工具和形式化基础仍由 Theorem 的人类工程师构建。

可信度来自可检查的证明，而不是模型声称自己写对了。

证明没完成，为什么也能找到 bug

Claude 在生成证明时遇到了数百个 bug，并获准自行修复。研究人员称，许多问题只在极特殊的条件下出现，例如异常大的输入文件，或者特定的访问顺序，常规测试很容易漏掉。

尝试证明程序满足要求，会迫使系统追查那些无法成立的路径。即使最后没能完成整个证明，这个过程也可能暴露真实缺陷。

原文给出两个例子：验证一个广泛使用的 PDF 阅读器时，团队一周发现的安全漏洞数量，相当于该软件通常一整年的报告量；另一个应用中的逻辑错误，则已经隐藏超过十年。

这些结果有吸引力，但原文没有提供具体软件名称、漏洞明细或统一的对照实验。我们能说的是，作者报告了明显的找错收益；还不能据此推导出，它对任意项目都比现有测试更有效。

为什么「通过验证」仍然有边界

Anthropic 自己承认，形式化验证不等于没有错误。这次证明依赖严格前提：特定处理器架构、单线程程序，以及小于 64 MB 的输入。实际部署中的库，可能运行在其他硬件和配置下。

证明的结论必须和前提一起读。

例如，单线程条件下成立的结论，不能直接拿来覆盖并发执行；输入小于 64 MB 的证明，也没有回答更大输入会怎样。原文还没有展开每项证明具体覆盖哪些性质，因此不能把它当成覆盖全部功能与安全要求的承诺。

成本同样限制落地。单个证明就可能消耗数亿 tokens，Anthropic 没有公布项目总费用。开发者是否能通过减少审查时间抵消这笔支出，目前缺少完整账单。

较小规模的试验显示，证明可以复用。模型效率也在改善：按原文表述，Opus 5.5 在其中一半证明任务上，比 Opus 5 少用约 40% 的 tokens。但这不代表整个验证流程的成本都下降了 40%。

Anthropic 预计，AI 形式化验证很快会像标准测试一样实用。Theorem 的路线图则指向 glibc、OpenSSL 和 cURL。前者是预期，后者是计划，都应与已经报告的实验结果分开看。

我的判断

我认可它把 AI 的输出接到独立检查程序上的方向。让模型找错、修改，再提交可机械检查的证明，比只让另一个模型阅读代码并给出评价，多了一层明确的验收依据。

但标题中的「自动证明安全」，比正文展示的范围更宽。实验主要处理已有软件，并且有架构、线程和输入大小限制；它尚未展示普通团队能以可接受成本，对日常 AI 生成代码普遍完成验证。

和单元测试、模糊测试相比，形式化验证的吸引力在于覆盖满足前提的情况，代价是必须明确前提、建立形式化基础，并承担计算成本。原文没有给出同等预算下的对照数据，所以「减少审查、降低整个编程流程成本」仍是待验证的推断。

对一般团队，更合理的定位是：它可能成为关键底层代码的额外保障。现有测试依然负责覆盖实际配置、集成行为和持续变更。

能拿来做什么

• 审查 AI 生成的代码时，把「正确」拆成可验收的具体要求，例如输入范围和错误处理行为，再判断现有测试覆盖了多少。
• 如果前端或 Node 服务依赖 PDF 解析、加密或网络传输相关的底层库，可以关注上游验证成果，但要核对版本和运行条件是否匹配。
• 团队评估类似工具时，先选择边界清楚的关键模块，记录验证范围、发现的缺陷、tokens 消耗和人工投入，再决定是否扩大使用。
• 阅读「已形式化验证」的宣传时，要求同时看到证明目标、适用前提和独立检查方式，避免把有限条件下的结论当成整个系统的保证。