Anthropic 用 Claude 自动生成形式化证明验证现有代码安全

Anthropic 用 Claude 以数学方式证明现有代码的正确性。该方法解决了 AI 生成软件的一个核心问题，但在实际应用中存在严格的限制。

证明软件在任何情况下都能无误运行，一直以来成本高得令人望而却步。一个专家团队仅为了形式化验证小型操作系统内核 seL4 就耗费了 20 个人年，因此这种方法只保留给 空客航空电子软件 这类极端场景使用。

Anthropic 的 Frontier Red Team 与合作伙伴 Theorem 合作，让 Claude 接手证明工作。该模型在短短几周内生成了约 1.8 亿行数学证明代码，参考了 Google OSS-Fuzz 安全项目中 123 个开源库的测试程序。

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

Claude 能发现多年测试都漏掉的 bug

在生成证明的过程中，Claude 遇到了数百个 bug，并被允许自行修复它们。研究人员说，其中许多 bug 会逃过常规测试，因为它们只在非常特殊的条件下才会出现，比如异常大的输入文件或特定的访问序列。

例如，在一次验证某个广泛使用的 PDF 阅读器的过程中，团队在一周内发现的安全 bug 数量，相当于该软件通常一整年报告的数量。在另一个应用中，Claude 发现了一个十多年来未被察觉的逻辑错误。Anthropic 表示，即使完整的证明最终失败，尝试过程仍能暴露出真实的 bug。

形式化验证能做什么、不能做什么

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

计算成本高昂，单个证明要消耗数亿 token。Anthropic 没有公布项目的总成本。但如果 AI 能验证自己写的代码，开发者就能更信任 AI 生成的软件，并减少审查时间。这不仅节省验证成本，还节省整个编码过程的成本。一次较小的测试还表明证明是可以复用的，而且更新的模型效率更高：Opus 5.5 用比 Opus 5 少约 40% 的 token 解决了一半的证明。

该项目强化了软件自动化的理由。如果 AI 既能编写代码，又能在确定条件下保证其正确性，那么问题就从“AI 能编程吗？”转变为“AI 能证明它写的代码是安全的吗？”如果答案是肯定的，其影响可能远远超出今天的编程工具。

一个例证：Anthropic 预计，借助 AI 的形式化验证很快就会变得和标准测试一样实用，而且 Theorem 的路线图 已经瞄准了 glibc、OpenSSL 和 cURL 等关键基础设施。

AI News Without the Hype – Curated by Humans

订阅 THE DECODER，享受无广告阅读、每周 AI 新闻通讯、每年六期的独家“AI Radar”前沿报告、完整档案访问权限以及评论区的发言权限。