fuzzer 跑了万亿次都没抓到的 bug，被写数学证明的 Claude 抓住了

软件行业有个著名诅咒：seL4，人类历史上验证得最彻底的操作系统内核，写代码用了 2 人年，形式化验证用了 20 人年。空客的飞控代码值这个价，剩下的 99.99% 软件不值。所以形式化验证 40 年来一直是安全领域的奢侈品：理论上它能"证明"代码没有某类 bug，实际上贵到没人用得起。

Anthropic 昨天发了一篇 Frontier Red Team 的研究，把这道算术题直接改了。他们让 Claude 对 Google OSS-Fuzz 计划里的 123 个开源库、239 个 fuzz 测试入口做形式化验证——证明这些编译后的程序对任意小于 64 MB 的输入、在所有建模的 Linux 系统响应和内存布局下，永不崩溃（无内存安全错误、无断言失败）。

结果是：几周时间，约 1.8 亿行 Rocq 证明代码，全部通过机器校验。典型一份证明约 60 万行，保护的是一个中位数只有 1.8 万条 RISC-V 指令的二进制文件。

还有副产品：证明写到哪，bug 抓到哪。抓出来的东西，是 fuzzer 永远不可能触发的。

▲ fuzzing 的工作方式：海量随机输入走同一个入口，撞到崩溃才算赢。画面里已经试了 332,168 个输入，找到 2 个崩溃——但搜索永远不完整（图源：Anthropic 原文视频，下同）

▲ 形式化验证的工作方式：不是试更多输入，而是把入口点可达的每一条路径都证明一遍。绿色=已证明无内存安全崩溃，红点=证明过程中浮出的 bug

一、最大的难题不是证明，而是"正确"到底是什么意思

形式化验证的第一步是写规格（spec）：什么叫"正确"？PNG 解码器好办——RFC 2083 写得很死。但文本编辑器、浏览器的"正确"是什么？没人能写出一个完备无歧义的规格。这是形式化验证规模化的第一块拦路石。

Anthropic 的解法很取巧：把开发者自己写的 fuzz 测试直接变成规格。OSS-Fuzz 的上千个项目，每个都有开发者手写的入口函数——任何能让它崩溃的输入都是作者在乎的 bug。Anthropic 把规则定义为："这个 fuzz 测试对所有小于 64 MB 的输入永不崩溃。"规格来源是现成的、权威的、而且覆盖内存安全这种通用属性。一旦证明成立，这个入口的 fuzzing 就永久退役——再也不用跑了。

技术上，开源库和它现有的 fuzz 测试被编译成 RISC-V 可执行文件，加上 Theorem 的 RISC-V 指令和 Linux 进程形式语义，机械地生成规格；Claude 负责写证明；Rocq 证明检查器负责校验。证明跑在汇编层面，不是源代码层面——这是他们认为的第一个在汇编层对生产软件做大规模 AI 形式化验证的尝试。源码编译器有没有 bug 都被覆盖进来了。

▲ 从代码到机器校验保证的完整流水线：源码+fuzz 测试 → RISC-V 可执行文件 → 机械生成的免崩溃规格 → Claude 写的 Rocq 证明 → 检查器确认。图中示例证明共 33 个文件、10.3k 行

二、1.8 亿行证明，为什么没人需要读一行

60 万行的证明怎么审？答案是不审。这是整个方法里最关键的一层认知：证明由 Rocq 内核机械校验，所以人只需要信任三个工件——

① RISC-V 和 Linux 进程的形式模型；② 被证明的定理陈述本身；③ Rocq 证明检查器。

剩下 1.8 亿行，全部是机器可丢弃的中间产物。剩下的 bug 只可能藏在上面三个工件里，或者在证明范围之外。而加固那三个工件，是一次性的、可复用的、不随项目数量增长的工作——验证一万个库，信任基还是那么大。Anthropic 把 RISC-V 语义、Linux 语义和不需要打补丁的完整证明都开源了。

三、fuzzer 的盲区，恰恰是证明的主场

证明过程中抓到的 bug，个个都在展示 fuzzing 的结构性盲区。fuzzer 变异小输入（通常上限 1 MB）、靠代码覆盖率导航，于是——

有一个解压器的计数器下溢，只在约 20 MB 且具备某种罕见特定布局的输入下才会越界写；有一个图像解码器的越界读，需要 64 MB 输入加 2 GB 内存；有一个越界读需要对同一文件的两个句柄按特定顺序调用——fuzzer 只会傻乎乎地顺序喂数据；还有在 libexpat 里重新发现 CVE-2026-56132，触发条件是深度嵌套的输入。这些东西的共同点是：输入空间大到 fuzzer 的采样概率约等于零，但对"所有路径"做归纳推理的证明绕开了采样。

还有不崩溃的逻辑 bug。证明某个库内存安全时，Claude 注意到一个"限制应用能加载哪些文件"的功能并不总是被强制执行。功能是对的，代码也没崩，安全属性破了——fuzzer 对这个无能为力，因为它根本不崩溃。

流程是全自动的：Claude 抓到 bug → 打补丁 → 规格基于补丁代码重新生成 → 继续证明新规格。当然，"AI 自己改代码再自己证明"有一个显然的作弊通道——把程序改成一个"永远不会崩溃"的空壳就算交差。团队对此的防范是：对任何 patch 施加惩罚，并对"证明 patch 改变了哪些输入、改变得多么少"给予额外加分；所有 patch 全部记录并审计。

值得补一句：要证明 cpp-httplib 的免崩溃，Claude 必须先排除 std::set 析构时递归过深导致栈溢出的可能，于是它在机器代码层面证明了 libc++ 的红黑树重平衡算法确实把树深度维持在对数界——一个连库的开发者都没要求过、但被免费赠送的属性。

四、不止内存安全：三条支线，三个信号

主项目之外，团队还放了三条支线。第一条，让 Claude 给 zlib 的 RFC 1950 格式写正式规格，然后证明 Linux 内核里的 zlib 实现（x86 编译产物）符合它——x86 的 ISA 语义也是 Claude 自己生成并重度测试的。结论很冷静：这些千锤百炼的代码库几乎已经全对，只挖出几个不可利用的边角 bug，正在上报上游。

第二条，用 Rust 写一个大型 Python 子集解释器，用 Verus 证明它遵循学术论文里写的 CPython 语义，再用 170 万个随机生成的 Python 程序做经验校验：99.95% 与 CPython 行为完全一致，剩下的差异全是已知边角。

第三条最猛：验证一个广泛使用的 PDF 阅读器，一周内发现的 security bug 数量相当于往年一年的上报量；其中一个是潜伏超过十年的未知逻辑 bug。

三个信号合起来读：形式化验证不只是"防崩溃工具"，它是一种系统性榨取代码真实语义的方法——你给它一个足够精确的规格，它就能把代码和规格之间的每一条缝隙都照出来。

五、规模化的两个杠杆：模型变强，证明复用

证明贵，贵在 token。单条证明动辄数亿 token。但两条曲线都在往下压。

第一是模型代际。团队用真实 OSS-Fuzz 代码构造了 36 个小验证任务：Opus 5.5 用约少 40% 的 token 就能证明其中一半，对比 Opus 5。同一张图上，Fable 5.1 介于两者之间。作者预期这个趋势会延续——尤其当训练数据里开始包含长验证任务时。

▲ 36 个验证任务的完成率随 token 预算的变化：Opus 5.5（橙）全面左移，约 40% 的 token 节省

第二是证明复用。证明和软件一样是递归结构——小证明拼成大证明，而小证明复用率极高。实验：让 36 个 agent 在同一个共享工作区里干活、允许互相抄已完成证明，结果平均省 17% token，且 34 个完成的证明里有 30 个比单干的平均成本更低，两个单干根本完不成的任务在共享区里完成了。放大到 OSS-Fuzz 主项目：大部分证明内容是每个程序都有的部分（C 运行时初始化、AddressSanitizer），agent 团队直接抄别人的证明改一改就用，共享部分几乎零新增代码。

▲ libcups、freerdp、libzmq 三个项目的证明构成：Allocator、Sanitizer runtime、共享库部分几乎逐字节相同（深蓝），真正的新证明（橙红）只剩"自己函数"那一块

这就是 Mathlib 的路径——Lean 数学库靠 700 多人攒出近 30 万条定理，每条新证明都站在旧证明上。软件证明的同构版本有一个额外的杠杆：依赖是幂律分布的。证明 glibc、OpenSSL、cURL 这一小撮共享库，就让一大片生态变得可证明。Theorem 已经放出了验证整个 Nix 生态的路线图。

六、边界：formally verified ≠ bug-free

这篇的局限性部分写得异常老实，值得逐条记住。第一，证明的对象是单线程、静态链接 musl libc 的 RISC-V 二进制，而你实际跑的是 x86 或 ARM、动态链接 glibc。规格和真机之间的差异，就是剩余 bug 的藏身之处。第二，ASan 检测不了所有内存 bug，入口点也没覆盖全，入口全覆盖也不等于覆盖整个库（还有死代码），而且调用方误用库造成的损坏在库的证明范围之外。第三，"证明无崩溃"依赖三个信任工件——它们本身也可能有 bug。

另一个容易忽略的彩蛋在脚注里：Claude 完全自主生成了 x86 ISA 的形式语义。质量怎么验证？拿它单步执行，能在 Linux 内核上把一个 Ubuntu 用户空间引导起来。生成语义的过程还顺手发现了官方 ISA 参考文档里的数百处错误，以及硬件本身的少量 bug。这件事的分量，值得单独一篇文章。

Theorem 向其他开源项目开放同一套流水线，还发布了一个 Claude skill 帮开发者验证自己的代码。Anthropic 最后给的建议很直白：以前试过形式化验证、当时觉得没用的开发者，值得用今天的模型再试一次。

七、我的几点想法

第一，这篇文章真正的标题其实不是"形式化验证"，而是"保证"的成本结构变了。安全攻防的荒谬现状是：攻击方的成本随 LLM 进步指数下降，防御方的"信心"却只能靠更多测试堆出来——而测试的本质是采样，采样永远不完整。证明是唯一非采样的防御手段，过去贵到人年，现在贵到 token。这两个单位之间的换算一旦成立，"关键依赖零已知崩溃"就会像今天的 CI 一样变成默认配置。文章里那句话我认为会兑现：验证将从 bolted-on 变成 built-in。

第二，"测试即规格"这个取巧是整个方法能落地的枢纽，值得单独品味。它绕开了 40 年来"规格写不出来"的死结，把定义正确性的权力交还给已经在写 fuzz 测试的开发者——你没多写一行规格，只是你写的测试突然升级成了数学命题。这提示了一种通用的工程模式：把既有的、分散的、非正式的人工制品，提升为形式系统的一等公民。

第三，证明复用 + 依赖幂律，意味着这条路线有明显的网络效应——先被证明的基础设施（glibc、OpenSSL）会被反复复用，后来者的成本持续下降。加上 Opus 5.5 的 40% token 节省，两条曲线叠加起来，"验证不过来的存量代码"这个量级的担忧要重新计算。

第四，冷静的地方也在这篇里：证明不覆盖 x86/glibc 实机、不覆盖调用方误用、不覆盖 ASan 盲区；"自己改代码自己证明"的作弊通道要靠罚 patch 加审计硬堵；1.8 亿行证明本身也可能是 reward hacking 的温床——只是 hack 一个机器可校验的证明，比 hack 一个人类评审难得多。这也是为什么"机器校验 + 小信任基"是整套方法的地基：它把信任的表面积压缩到了三个工件上。

最后一句给做安全的读者：当 fuzzing 在一个 PDF 阅读器上一周挖出一年的量，这件事对攻击方同样成立——区别只在于，防御方现在可以问出攻击方永远不用回答的问题：你能证明没有了吗？