Anthropic 用 Claude 自动证明代码安全

Anthropic 利用 Claude 从数学上证明了现有代码的正确性。这种方法解决了 AI 生成软件的一个核心问题，但也伴随着严格的实际限制。

证明软件在所有情况下都能无误运行，历来成本高昂得令人却步。一个专家团队仅为了对小型操作系统内核 seL4 进行形式化验证，就耗费了 20 人年的时间，因此这种方法通常只用于极端场景，例如 空客航空电子软件。

Anthropic 的 前沿红队（Frontier Red Team）与合作伙伴 Theorem 合作，让 Claude 接管了证明工作。该模型在短短几周内生成了约 1.8 亿行数学证明代码，这些代码基于谷歌 OSS-Fuzz 安全项目中来自 123 个开源库的测试程序。

Claude 并非编写新代码，而是通过验证现有软件来工作：它将崩溃测试转化为数学问题，分析编译后的机器码，并生成详尽的证明。一个名为 Rocq 的独立验证程序会自动检查这些证明，据 Anthropic 称，这一过程几乎不需要人工审核员。研究人员将其称为“完全自主”的证明生成，尽管相关工具和形式化基础是由 Theorem 的人类团队构建的。

Claude 发现了多年测试未能捕捉到的漏洞

在生成证明的过程中，Claude 遇到了数百个漏洞，并被允许自行修复它们。研究人员表示，许多漏洞本会逃过传统测试，因为它们仅在非常特定的条件下才会显现，例如异常大的输入文件或特定的访问序列。

例如，在尝试验证一款广泛使用的 PDF 阅读器时，团队在一周内发现的安全漏洞数量，相当于该软件全年通常报告的漏洞总数。在另一个应用中，Claude 捕捉到了一个十多年未被发现的逻辑错误。Anthropic 表示，即使最终无法完成完整的证明，这一尝试仍然能暴露出真实的漏洞。

形式化验证能做到什么，不能做到什么

Anthropic 承认，“形式化验证”并不等同于“零错误”。这些证明仅在严格条件下成立：特定的处理器架构、单线程程序以及小于 64 MB 的输入。而在实际应用中，这些库往往运行在不同的硬件和配置环境中。

计算成本高昂，单个证明过程可能消耗数亿个 token。Anthropic 未披露项目的总成本。但如果 AI 能够验证其自身生成的代码，开发者就能更信任 AI 生成的软件，并减少审查时间。这不仅节省了验证成本，还能降低整个编码流程的成本。一项小规模测试还表明，证明具有可复用性，且新模型的效率正在提升：Opus 5.5 解决一半的证明任务所需的 token 数量比 Opus 5 减少了约 40%。

该项目强化了软件自动化的论点。如果 AI 既能编写代码，又能在特定条件下保证其正确性，那么问题的焦点就从“AI 能否编程？”转变为“AI 能否证明其编写的代码是安全的？”。如果答案是肯定的，其影响将远超当前的编码工具范畴。

一个典型的例子是：Anthropic 预计，结合 AI 的形式化验证很快将变得像标准测试一样实用，而 Theorem 的路线图 已经瞄准了 glibc、OpenSSL 和 cURL 等关键基础设施。