Anthropic正尝试让AI不只写代码，还能用数学方法证明代码正确。该公司前沿红队与合作伙伴Theorem合作，利用Claude对现有开源软件进行形式化验证，在数周内为123个开源库生成了约1.8亿行数学证明代码，并在此过程中发现并自行修复了数百个常规测试未能捕捉的缺陷。

形式化验证长期被视为成本极高的手段。此前，一个专家团队需要20人年才能完成小型操作系统内核seL4的完整验证，因此这类方法通常只用于空中客车航电软件等极端关键场景。Anthropic此次的思路是让Claude接管证明工作：模型不写新代码，而是把Google OSS-Fuzz安全项目中的测试程序转化为数学问题，分析编译后的机器码，并生成大量证明。独立验证程序Rocq会自动检查这些证明，Anthropic称整个过程几乎不需要人工复核。

在生成证明的过程中，Claude遇到了数百个缺陷，并被允许自行修复。研究团队表示，许多缺陷只有在非常特定的条件下才会暴露，例如异常大的输入文件或特定的访问顺序，因此常规测试很难发现。在验证一款广泛使用的PDF阅读器时，团队在一周内发现的安全缺陷数量，与该项目通常一整年报告的数量相当。另一个应用案例中，Claude捕捉到一个隐藏了十多年的逻辑错误。Anthropic还指出，即使最终证明失败，尝试过程本身也能暴露真实缺陷。

不过，Anthropic明确承认，“形式化验证”并不等于“没有错误”。这些证明只在严格条件下成立：特定的处理器架构、单线程程序，以及输入小于64MB。现实中，这些库运行在不同的硬件和配置上。计算成本也相当高，单个证明可能消耗数亿个token，Anthropic未披露项目总成本。

从行业角度看，这项实验的意义在于把AI编程的讨论从“AI能否写代码”推进到“AI能否证明自己写的代码安全”。如果开发者能更信任AI生成的软件，并减少人工审查时间，节省的将不只是验证成本，还包括整个编码流程的开销。Anthropic还提到，较小规模的测试显示证明具有可复用性，且新模型效率在提升：Opus 5.5完成一半证明所需的token比Opus 5少约40%。

Anthropic预计，AI形式化验证很快会变得像标准测试一样实用。Theorem的路线图已瞄准glibc、OpenSSL和cURL等关键基础设施。但这一愿景能否落地，取决于证明条件能否覆盖真实世界的复杂运行环境，以及算力成本能否降到可规模化复用的水平。