Claude写了1.8亿行Rocq证明，挖出模糊测试万亿次没碰到的漏洞

Anthropic 和 Theorem Labs 合作做了一件很“苦”的事：让 Claude 直接对着 RISC-V 汇编，给开源软件做形式化验证。

几周时间，覆盖 123 个开源代码库、239 个测试入口，产出了 1.8 亿行通过核验的 Rocq 证明代码。Rocq 就是以前的 Coq，一个定理证明器。

这个工作量放在过去是不可想象的。机器码级别的形式化验证一直是安全圈公认的“正确但没人做得起”，一个中等规模的库就能耗掉一个团队几年。

结果也挺吓人。

他们挖出了一批模糊测试跑了上万亿次都没碰到的漏洞，有些高危逻辑问题埋了十几年；还顺手发现了 x86 处理器层面的硬件缺陷，以及官方文档里写错的地方。

原理不复杂。模糊测试是随机喂输入，看程序崩不崩，本质是抽样，总有漏网的。形式化验证是把测试入口翻译成数学命题，要求对所有路径、所有输入都给出证明。证明在哪里推不下去，哪里多半就有问题。Claude 卡住以后还会尝试写补丁，补完接着往下证。

成本上的说法是：这类验证的效率现在大约每两个月翻一倍，写出来的证明还能在项目之间复用。按这个趋势推，投入约 1.34 亿美元，2027 年底能把 Nix 生态 95% 的机器码验证一遍。第一批证明已经公开。

这周 PHP 刚因为 AI 挖出来的漏洞闹得全球运维通宵，现在又来一个。找漏洞这件事，攻防两边都在用模型，区别是谁先把补丁打上。