Claude 把 239 个模糊测试改写成证明：123 个开源库在 RISC-V 二进制层面被证「64 MB 内任意输入都不崩」，约 1.8 亿行 Rocq

从「跑得越久越安心」到「证完就不用再跑」

模糊测试的思路是往一个测试入口灌海量随机输入，看哪个能把程序弄崩。它跑得越久找到的缺陷越多，但永远无法穷尽。Anthropic 前沿红队 10 月 22 日发布的研究换了个做法：把 OSS-Fuzz 里开发者写好的测试入口直接当成规约，即「这个入口对任何小于 64 MB 的输入都不会崩溃」，让 Claude 去证明它成立。

证明针对的是编译后的 RISC-V 指令，而不是源码。合作方 Theorem 提供 RISC-V 指令和 Linux 进程的形式化语义，Claude 写证明，Rocq 证明检查器负责核对。几周内，Claude 在 123 个库的 239 个入口上完成了证明，总量约 1.8 亿行 Rocq，典型证明约 60 万行，对应的二进制中位数约 1.8 万条指令。这么大的证明不需要人逐行审：需要信任的只有 RISC-V 与 Linux 模型、定理陈述本身和 Rocq 检查器。

证明途中挖出的缺陷

证不下去的地方往往就是缺陷，Claude 被允许直接打补丁再继续证，于是顺手找出了数百个问题。有些是模糊测试几乎碰不到的：一个解压器拷贝里的计数器下溢导致越界写，只在约 20 MB、布局特殊的输入下触发，而模糊器通常把输入限制在 1 MB 内；一个图像解码器的越界读需要 64 MB 输入和 2 GB 以上内存；还重新发现了 libexpat 的 CVE-2026-56132。为防止 Claude 把程序改成「什么都不做所以不会崩」来骗过证明，团队对补丁扣分并逐个审计。

边界写得很清楚

文章专门列了局限：证明假设程序是单线程静态二进制、链接 musl、跑在 RISC-V 上，而多数人实际用的是 x86 或 ARM 加动态链接的 glibc；AddressSanitizer 本身抓不到所有内存错误，也没有覆盖每个库的全部入口。成本同样是门槛，证明动辄消耗数亿 token。Anthropic 给出的两个下降信号是：36 个小型验证任务里，Opus 5.5 证完一半所需 token 比 Opus 5 少约 40%；让智能体共享工作区互相复用证明，token 再省 17%。

不涉及修补的那部分证明、RISC-V 与操作系统语义已经公开，可能暴露未修补缺陷的证明暂不发布；Theorem 表示愿意为其他开源项目跑同一套流程。对维护底层库的团队，现实的用法可能不是追求「全证完」，而是先把它当成一种能找到模糊器盲区的缺陷挖掘手段。