Claude 写出 1.8 亿行数学证明：Anthropic 首次大规模验证开源软件底层安全

全文

Anthropic 10 月 22 日在官方研究页面公布：与软件验证公司 Theorem 合作，用 Claude 在 RISC-V 汇编层面对 123 个取自 Google OSS-Fuzz 的真实开源库、239 个程序入口做了安全性形式化验证。据其称，这是「AI 对生产级软件做汇编级形式化验证的首次大规模尝试」。

规模惊人：共生成约 1.8 亿行 Rocq 证明，典型证明约 60 万行，覆盖中位数 1.8 万条 RISC-V 指令的二进制文件；全部在几周内完成。证明由 Rocq 内核独立校验，无需人工逐行审查。

方法是把现有的 fuzz 测试转成数学规范：64MB 以下任意输入、单线程静态链接的 RISC-V 二进制、Linux 环境下必须正常退出、无内存安全违规。证明过程中若发现疑似 bug，Claude 直接打补丁再重新证明。

挖出的 bug 有数百个：包括在某解压器的拷贝中发现计数器下溢导致的越界写入（需约 20MB 特定布局输入才能触发）、图像解码器中的越界读取，以及 libexpat 中 CVE-2026-56132 的重新发现——有些漏洞已潜伏多年。

Anthropic 自己也承认局限：「形式化验证通过」不等于没有 bug——证明只覆盖单线程静态 RISC-V 二进制，而多数代码实际跑在 x86/ARM 上。不过它已把部分证明发布到 GitHub 供独立验证，Theorem 也表示愿为其他开源项目跑同样的流水线。

副成果同样亮眼：证明了 Linux 内核 zlib 实现在 x86 二进制层符合 RFC 1950；用 Rust 写的 Python 解释器大子集与 CPython 在 170 万＋随机程序上行为一致率达 99.95%。