Claude 完成 1.8 亿行形式化证明：从找 Bug 推进到给定条件下证无 Bug

核心事实：Anthropic 前沿红队与 Theorem 用 Claude 为 123 个开源库的 239 个测试入口生成约 1.8 亿行形式化证明，并发现数百个 bug。

• 规模与验证路径：库与测试被编译为 RISC-V 机器码，Theorem 生成命题，Claude 写证明，Rocq 逐行检查。单份证明通常约 60 万行，对应程序中位数约 1.8 万条机器指令。
• 发现的缺陷：证明卡住处常对应真 bug，Claude 可自行打补丁并重新证。已披露案例包括解压器计数器下溢（需约 20MB 刁钻输入）、图像解码器越界读（需 64MB 输入与 2GB 以上内存），以及重新发现 libexpat 的 CVE-2026-56132。
• 成本与开放：一套证明可能消耗上亿 token；Opus 5.5 证完一半任务比 Opus 5 少约 40% token，多 agent 共享工作区复用证明再省 17%。Theorem 发布 Claude skill，并开放 OSS Verify 供符合条件的开源项目免费跑这套流水线。
• 边界：当前只覆盖 RISC-V 特定打包版本和部分入口，只保证程序不崩溃、内存不越界，不保证计算结果正确；AI 自改代码需审计，补丁会按影响面扣分。
• 行业意义：形式化验证过去因成本高，主要用于空客航电等失效代价极高的代码；这次把流程压缩到数周，并给出可公开复用的工具链。它的意义不是宣布“零 bug”，而是让防守方能在给定条件下规模化证明某条路径没有特定类型缺陷。 🔗 原文