Anthropic 用 Claude 自动生成约 1.8 亿行数学证明代码验证现有软件安全性

Anthropic 用 Claude 对百余开源库完成汇编级形式化验证

2026 年 10 月 22 日，Anthropic 发布 Frontier Red Team 博客新研究，与 TheoremLabs 合作，用 Claude 在数周内为一百多个真实开源库证明安全属性。形式化验证可证明代码不存在特定 bug，但此前仅适用于小型代码库或需大量专家时间，AI 模型正改变这一局面。10 月 23 日的官方博客跟进披露更多细节：团队对 123 个开源库在 RISC-V 汇编代码层面证明安全性质，包括程序在特定条件下不会触发内存安全错误或断言失败，作者称这是首次大规模用 AI 对生产软件做汇编级形式化验证；过程中 Claude 还发现了多年未被检测到的 bug，团队为防 reward hacking 对任何补丁施加惩罚，并奖励证明补丁未改变程序行为。同日 The Decoder 报道称，Claude 将崩溃测试转化为数学问题、分析机器码并生成约 1.8 亿行证明，由 Rocq 独立自动校验，几乎无需人工复核；验证某广泛使用的 PDF 阅读器时，一周发现的安全漏洞相当于其一年报告量，还抓到一个潜伏十余年的逻辑错误。报道同时指出限制：证明仅在特定处理器架构、单线程和 64 MB 以内输入下成立，单个证明耗资最高数亿 token；Opus 5.5 比 Opus 5 用约少 40% 的 token 解决一半证明；Theorem 计划将方法推广到 glibc、OpenSSL 和 cURL。