Anthropic 让 Claude 自动为代码生成形式化安全证明

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

证明软件在所有情况下都能无错误运行一直非常昂贵。一个专家团队需要 20 人年 才能正式验证小型操作系统内核 seL4，因此该方法仅保留用于极端情况，如 空客航空电子软件。

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 使用大约 40% 更少的 token 解决了大约一半的证明。

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

例如：Anthropic 预计，AI 的形式验证将很快变得与标准测试一样实用，而 Theorem 的路线图 已经针对 glibc、OpenSSL 和 cURL 等关键基础设施。

AI 新闻无炒作——由人类编辑

订阅 THE DECODER 以享受无广告阅读、每周一份的 AI 新闻简报、我们独有的每年六次的 "AI 雷达" 前沿报告、完整档案访问权限以及访问我们的评论区。