一百二十三个库，证到不会崩

10 月 23 日凌晨 6 点 01 分（北京时间），Anthropic 的官方账号发出一条：用 Claude 在「一百多个」真实开源库里证明安全性质，用时几周。1 研究页把数字写细了：123 个开源库、239 个测试入口、约 1.8 亿行通过检查的 Rocq 证明。2

这条消息最容易被读成「AI 把 bug 消灭了」。原文「局限」一节的第二句就拦住这个读法：「This doesn't mean these libraries contain no bugs.」2 这篇文章做一件事——把「证明了什么」与「没证明什么」分开写。在这份工作里，这两件事是同一条定理的两面。

先说被证的东西。Claude 证的不是「这个库功能正确」，而是一条范围写死的性质：对任何小于 64 MB 的输入，程序不会触发内存安全错误，也不会触发断言失败。前提是它作为单线程静态二进制运行，有固定内存预算，跑在 RISC-V 的 CPU 上、Linux 里。2

技术上它其实是三条定理串起来：ASan 插桩版不崩；插桩版与普通版在四种可观测量上行为等价；于是普通版也不崩。3

一句大白话：它证的是「不会崩」。在任何输入下都不崩，当然比「跑过一百万条测试没崩」强——fuzzing 是抽样，抽样永远可能漏掉那条能崩的输入；证明是全量，只要它覆盖的假设成立。

代价是体积。被证程序的中位数是 18,000 条 RISC-V 指令，一份典型证明约 60 万行 Rocq，分在约 1,400 个文件里，各库从 33 万行到 90 万行不等。3 更极端的是 cJSON：一个 391 行的解析入口，换来 63 万行证明，而其中只有约十分之一与 cJSON 本身有关，其余是每个程序共有的运行时与 ASan。3

这也解释了为什么过去只有最要命的地方才做形式化验证：证明比代码大三十多倍是常态。

形式化验证最难的一步从来不是写证明，是说清「什么算对」。历史上这一步全靠人。seL4 微内核的实现是 2.2 人年，形式化验证是 20 人年。4

这次的做法绕开了写规格：直接捡现成的。OSS-Fuzz 里的每个测试入口都由代码作者自己写，定义是「任何让它崩掉的输入都是 bug」。于是规格可以写成一句机械的话——「这个入口的 fuzz test 在任意小于 64 MB 的输入下都不会崩」。整个流程是：把库和它的测试编译成 RISC-V 静态可执行文件，ASan 负责把内存错误变成崩溃，Theorem 提供 RISC-V 指令与 Linux 进程的形式语义，这条定理就被机械地生成了。2

接下来的活交给模型：Claude 写 Rocq 证明脚本，Rocq 的 kernel 逐条检查，通不过就不是证明。几周里覆盖了 239 个入口。

这个做法有个副产品。证明走不通的地方，就是一个真的能崩的输入——反例本身就是 bug。原文的流程因此是循环的：发现崩溃、修掉、用修好的代码重新生成定理、再证。它找到的东西包括一个只在约 20 MB 罕见输入布局下出现的下溢越界写，一个需要 64 MB 输入与 2 GB 内存才触发的越界读，还有一个要跨两个文件句柄按特定顺序调用才出现的越界读；此外它重新发现了 libexpat 的 CVE-2026-56132。2 这些形状 fuzzing 很难碰到，因为 fuzzer 的输入通常被压到 1 MB 以内。

所以在附录里，作者特别写了一句话给外部项目：一个证明只和它的 fuzz target 一样强；弱的 fuzz target 会让定理变成空话。5

便宜的到底是什么？不是证明本身便宜了，是「什么算对」这件事被一条现成的测试替代了。这也决定了射程：你能证的，只能是别人已经写成测试的那些性质。

原文对成本的表述只有一句，但很硬：这类证明可能要消耗数亿 token。2 附录再补两个数字：整个项目 Claude 一共写了约 10 亿行 Rocq，其中 1.8 亿行进到通过检查的证明里；单份证明过一次检查要 30 分钟到数小时 CPU。3

这些数字没有对应的价目表。我按 Anthropic 公开的 API 单价（Opus 5.5 输入每百万 token 4 美元、输出 20 美元）6 粗算了一次：把「数亿」依次当作 1 亿到 10 亿 token、输出占一成到三成，一份证明的账单大致落在 560 到 8,800 美元；用更贵的 Fable 5.1 算，上限到 2.2 万美元。239 个入口整批下来，十几万到几百万美元之间。这是估算，原文没有给金额。3

拿它和人工比一下：seL4 的 20 人年，按每人年 20 万美元全成本折算约 400 万美元，对应的是一万行左右的内核。4 也就是说，这次 123 个库、1.8 亿行证明的账单，与当年一个内核的验证费用同量级。便宜的不是单价，是单位代码的覆盖量。

合作方 Theorem 自己也在博客里算过这笔账：按每 KB 机器码 40 美元、每小时验证 0.5 KB 的成本模型，到 2027 年底验证 nixpkgs 95% 的机器码要约 1.34 亿美元；OpenSSL 一份证明约 22 万美元，或按复用它的包摊到 14 美元。7 这是模型不是报价，但如果它接近现实，形式化验证的费用结构会从「项目」变成「单价」。

成本在动，方向往下。Anthropic 用 36 个从真实 OSS-Fuzz 代码里裁出来的小任务做了对照：每个任务给三次独立尝试、每次 5M token 预算。Opus 5.5 证出一半，比 Opus 5 少用约四成 token；让代理共享工作区、互相抄已经写完的证明，token 再少 17%，34 个完成的证明里 30 个比单干便宜。2

复用逻辑指向一个具体的商业判断：依赖是幂律分布的，把那几个所有人都在用的库证掉，可证的软件一下多出一大片。Theorem 公开的路线图就是拿 Nix 生态开刀，里面包括 glibc、OpenSSL 和 cURL。7

原文把限制写得很直白，我按它的顺序列：

机器不一样。 证明说的是单线程、静态链接 musl libc 的 RISC-V 二进制；多数人跑的是 x86 或 ARM，动态链接 glibc。2

范围不全。 ASan 查不出全部内存安全 bug；每个库也不是所有入口都证了；即使全证了，死代码也不在其中。

调用方不在里面。 库被误用、在调用方造成的破坏，这条定理管不到。

64 MB 是参数。 脚注说，改这个上界只需要「trivial human effort」：改参数、重新生成定理、让 Claude 重证。2

还有一层要信的东西。 一份证明跑完，开发者真正需要相信的只有三样：RISC-V 与 Linux 进程的形式语义、被证的那条定理陈述本身、Rocq 的 kernel。脚注补了一句更老实的：严格说还得信硬件、操作系统，和跑 Rocq 检查器的那个 OCaml 编译器。2

原文的总结是：proof checker 无法告诉你规格是否与现实相符；被验证的代码出问题时，问题总是出在规格或者机器语义与现实不一致的地方。它顺带给出了排查方向——出了事，先查那三样，而不是重读那 60 万行证明。

比原文更硬的清单在 Theorem 的仓库里。RISC-V 与 Linux 的语义仓库自带一份 SCOPE.md，写明这套模型只支持 Linux v6.18.46 与 QEMU 用户态、RV64GC；单线程、没有调度器、不跑信号处理函数；文件模型没有完整目录树、没有符号链接、没有权限；参数里不得含 /，所以 cp src dst 的证明不适用于 cp /tmp/src dst；二进制必须是静态 ET_EXEC，静态 PIE 会算错 program break。它还写了一句最要命的：规格与检查器若犯同一个错，「An error in both gives a correct proof of the wrong thing」。8

还有一条容易被忽略：公开的证明仓库自己写着，这批证明里没有一条证明了「程序会终止」，所以「一次永不结束的运行」没有被排除。9 而摘要里那句「always exit normally」很容易被读成它证了终止。

最后一层是激励。原文在讲代理自动修 bug 时承认，这给 reward hacking 留了门。2 六天前，Galois 的实测记录把这件事写成了具体动作：模型证不出也证不伪的时候，开始删定理。10 一个把「证出来」设成目标的系统，天然会奖励「看起来证出来了」。

研究覆盖 239 个入口、123 个库。公开的证明仓库写的是另一组数：60 个入口、25 个库。9 原文解释了差额——可能暴露未修漏洞的证明不公开。这个理由成立，但它同时意味着：外人能独立复算的部分，是标题数字的四分之一。

截至目前，没有人贴出复算结果。Hacker News 上这条帖到 10 月 23 日 06:36 UTC 是 264 分、约 150 条评论；11 评论里有关于「证的是不崩而不是功能正确」的争论，也有人追问 RISC-V 与 Linux 的形式模型到底是什么，但没有人说自己把仓库拉下来跑过一遍。唯一做了仓库级核算的是一篇独立分析，它把「研究口径」和「公开子集」分开数，并明确写自己也没有复跑。12

媒体那一侧也值得记一笔。发布后两小时，跟进的是 Unite.AI 与 kingy.ai 这类垂直站；13 TechCrunch、Ars Technica、The Register、The Verge、VentureBeat 在发布后 24 小时内的站内检索里都没有自有稿。中文侧同样检索不到机器之心与量子位的稿子。这不是说这条消息不重要，而是说它的读者面目前还停在安全与形式化方法的圈子里。

三类人受影响的方式不一样。

开源维护者拿到的是产能。Theorem 的 OSS Verify 对合格项目免费，报名走一个 pull request，要求 OSI 认可的 license、至少一个 fuzz target、能构建成静态 riscv64 二进制；他们不设披露期限，也不公开发现，只私下报给维护者。14 门槛写在明处：只有核心维护者能报名，二进制 .text 小于 1 MB 的项目会更快。

企业采购要改的是验收口径。「我们形式化验证过」这句话本身没有信息量，有价值的是三样产物：定理陈述、信任基座、被排除的清单。同一个词底下，可能是一条覆盖 239 个入口的内存安全定理，也可能只是一段关键路径的功能证明。Theorem 的商业侧只有一句 Talk to us，没有公开价。14

安全团队不用换工具链，但要换预期。形式化验证覆盖的是你写出来的性质；没写出来的部分，它一句话都不说。fuzzing 仍在负责「找没想到的」，只是在被证明覆盖的那一段入口上，fuzzing 从此是冗余的。

合规那一侧还没有落点。CISA 牵头的内存安全倡议是「强烈鼓励」，公开的采购清单里没有「形式化验证」这一项；15 欧盟的 CRA 与 AI Act 全文里也找不到这个词。16 也就是说，今天买它靠的是工程判断，不是监管压力。

能确定：官方帖发布于 10 月 22 日 22:01:06 UTC，页面首版在 21:59:17 UTC 已定稿，22:01:19 UTC 已有含全文的公开存档；1 123 个库、239 个入口、约 60 万行一份、10 亿行生成 / 1.8 亿行通过、18,000 条指令中位数、64 MB 上界、五条假设与三样信任基座，都是原文与附录逐字。23

不能确定的有五处。第一，独立复核没有出现：证明仓库与语义仓库都公开了，但没有第三方贴出复算结果。第二，「第一次在机器码层面对生产软件做大规模形式化验证」是作者的自述（原文写 to our knowledge），没有第三方认证；能确证的只是「用 LLM 写形式化证明」这件事此前已有先例。第三，钱：原文只给「数亿 token」这个量级，没有金额，也没有说这是单个证明还是整批。第四，公开的 60 个入口是否足以代表那 239 个，只有官方一句「扣下可能暴露未修漏洞的证明」。第五，复用的实际折扣，目前只有 34 个证明的小样本与 17% 这个数。

可以确定方向的一件事是：如果这条路真的走通，软件供应链的验收会从「扫描报告」变成「定理清单」。到那时候，值得问的还是同一个问题——这条定理，证的是什么，没证什么。