Anthropic 让 Claude 自动为现有代码生成安全证明

Anthropic 用 Claude 对现有代码进行了数学证明，确认其正确性。这一方法解决了 AI 生成软件的一个核心难题，但在实际应用中存在严格的限制。

要证明软件在所有情况下都不出错，成本一直高得令人望而却步。一个专家团队花了 20 人年，才完成对小型操作系统内核 seL4 的形式化验证，因此这种方法此前只用于 Airbus 航空电子软件这类极端场景。

Anthropic 的 Frontier Red Team 与合作伙伴 Theorem 联手，让 Claude 接管了证明工作。该模型在几周内产出了约 1.8 亿行数学证明代码，所用材料来自 Google 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 等关键基础设施列为目标。

没有炒作的 AI 新闻——由人类精选

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