Claude 写完代码还能自动证明它正确

过去要给软件做数学层面的正确性证明，验证一个小型操作系统内核 seL4 就花了约 20 个人年，所以这套方法长期只出现在空客航电这类极端场景。现在 Anthropic 让模型来干这个活，几周干了过去一个团队十几年的量。

一、发生了什么

10 月 23 日据 The Decoder 报道，Anthropic 的前沿红队与合作伙伴 Theorem 让 Claude 给既有软件生成正确性证明：它把崩溃测试转成数学命题，分析编译后的机器码，再写出完整证明，由独立程序 Rocq 自动核验。官方称过程几乎不需要人工审阅，但工具链和形式化基础仍是 Theorem 的人搭的。

规模不小：几周内产出约 1.8 亿行证明代码，素材来自谷歌 OSS-Fuzz 安全项目里 123 个开源库的测试程序。写证明的过程中，Claude 顺带抓到数百个常规测试多年没发现的漏洞，并且获准自己修。验证一款广泛使用的 PDF 阅读器时，一周发现的安全漏洞数量相当于该项目往年一整年的报告量；另一个应用里，一个藏了十多年的逻辑错误被翻了出来。

二、跟你有什么关系

用 AI 写代码的开发者。 代码审核是最贵的环节。如果模型能对定义好的条件给出证明，你抽查的范围可以收窄。Anthropic 的判断是，AI 辅助形式化验证很快会像跑测试一样平常。

维护开源组件的人。 小规模实验显示证明可以复用，新模型也在变便宜：Opus 5.5 用比 Opus 5 少约四成的 token 解出一半的证明。

安全团队。 证明失败也有价值——过程中暴露的都是真实漏洞，等于一次不知疲倦的深度审计。那些只在超大输入文件或特定访问顺序下才触发的错误，恰恰是常规测试最难覆盖的盲区。

三、怎么判断

1. 别把「已验证」读成「无缺陷」。证明只在严格前提下成立：特定处理器架构、单线程、输入小于 64MB。真实部署环境大多不满足，边界外的风险照旧。
2. 算算成本账。单条证明可能烧掉数亿 token，Anthropic 没公布项目总开销。核心库、高频复用的组件值得，业务代码未必。
3. 关注 Theorem 的路线图：目标是 glibc、OpenSSL、cURL 这类关键基础设施。它们一旦被验证，全行业都受益。

四、三个别信的说法

错误说法一：软件 bug 从此终结。 证明覆盖的只是定义过的条件和单一执行路径，并发、异构硬件、超大输入都不在保证范围内。测试依然要跑。

错误说法二：AI 全自动证明了代码，人类可以退场。 「全自动」的前提是 Theorem 预先搭好的工具和形式化框架。没有这套地基，模型自己写不出可被机器核验的证明。

错误说法三：这和普通安全扫描是一回事。 扫描器找已知模式的漏洞，证明是穷尽地排除一类错误在特定条件下的全部可能。后者贵得多，但也严格得多。

五、一句话结论

从「AI 会写代码」到「AI 能证明代码没错」，软件质量的裁判权正在换手。

信息来源

• The Decoder：Claude 自动生成代码正确性证明（2026-10-23）

功能与价格以官方公告为准。本文写于 2026 年 10 月 24 日。