Anthropic 让 Claude 为 123 个开源库写下数学证明

发生了什么

起点是谷歌 OSS-Fuzz 项目给开源库写的模糊测试条目。Claude 把每个测试条目转成一条形式化规约——“该测试在 64MB 以内输入下永不崩溃”，针对编译出的 RISC-V 可执行文件写出 Rocq 证明，再由 Rocq 内核机械校验；Theorem 提供 RISC-V 指令与 Linux 进程的形式化语义模型。全部写证明的中间产物累计约 10 亿行，最终成稿约 1.8 亿行，典型证明约 60 万行，对应中位数 1.8 万条 RISC-V 指令的二进制。

证明写不下去时，往往意味着真有一个 bug：Claude 直接修代码、重新生成规约、再证明。过程中挖出的例子包括一个只在约 20MB 特定布局输入下触发越界写的解压库计数器下溢、需要 64MB 输入和 2GB 以上内存的图片解码器越界读、libexpat 中 CVE-2026-56132 的重现，以及一个潜伏十多年的未知逻辑 bug。团队还顺带形式化了 RFC 1950，并证明 Linux 内核的 zlib 实现在 x86 二进制层面符合该规范。

Anthropic 已在 GitHub 公开部分证明与 RISC-V/OS 语义；Theorem 表示可为其他开源项目运行同样的管线，并发布了一个 Claude skill 帮助开发者验证自己的代码。研究由 Anthropic Frontier Red Team 与 Theorem 共同完成，团队称据其所知，这是首次以 AI 在生产级软件的汇编层面做大规模形式化验证。

关键事实

1. 发布：2026 年 10 月 22 日，Anthropic 研究博客（Frontier Red Team）与形式化验证公司 Theorem 联合发布，标题《LLMs are making formal software verification feasible at a much larger scale》
2. 规模：239 个测试入口、123 个谷歌 OSS-Fuzz 开源库；约 1.8 亿行 Rocq 证明（典型证明约 60 万行，中位数二进制长 1.8 万条 RISC-V 指令）；数周完成
3. 证明内容：针对编译后的 RISC-V 汇编指令，在输入小于 64MB、单线程静态链接二进制、固定内存预算、Linux 环境的假设下，程序正常退出、不触发内存安全错误、不失败断言；Rocq 内核机械校验
4. 挖出 bug：数百个，多数模糊测试难以命中——约 20MB 特定布局输入才触发的解压库计数器下溢（越界写）、需 64MB 输入加 2GB 内存的图片解码器越界读、libexpat 的 CVE-2026-56132 重现、潜伏十多年的未知逻辑 bug；一个常用 PDF 阅读器一周挖出的安全 bug 相当于其通常一年的报告量
5. 对照：seL4 微内核实现花了 2 人年，形式化验证花了 20 人年；本工作把同量级的工作压缩到数周
6. 局限（公司自述）：证明的是编译后的特定 RISC-V 程序，不等于“无 bug”——大多数人实际跑的是 x86/ARM 且动态链接 glibc；ASan 检不出所有内存安全问题；每个库并非所有入口都验证了
7. 后续：部分证明与 RISC-V/OS 语义已在 GitHub 公开；Theorem 为其他开源项目提供同款管线并发布 Claude skill