Claude 写了 1.8 亿行证明，让 123 个库不会崩，这是本周防守方的回答

10 月 22 日，Anthropic 的 Frontier Red Team 发了一份形式化验证成果，数字大得让人愣一下。和 Theorem 合作，Claude 给 OSS-Fuzz 里 123 个开源库的 239 个入口函数证明了不会崩溃，而且是在 RISC-V 二进制层面验证的。证明总量约 1.8 亿行 Rocq，单个证明通常就有 60 万行左右。链接：https://www.anthropic.com/research/formal-verification

可信基被刻意压得很小：你只需要相信 RISC-V 和 Linux 的模型、定理陈述本身、以及 Rocq 检查器，别的都不用信。Claude 没有给自己打分的机会。证明过程中它顺手修了挡路的 bug，其中有些 fuzzer 几乎碰不到，因为要 20MB 左右的输入、或者 64MB 和 2GB 这种内存配置才能触发；它还重新发现了一个已知的 libexpat CVE。另一个支线拿 Rust 重写的 CPython 跟原版对比，170 万个随机程序里 99.95% 行为一致。

对大规模跑 agent 的人，有两个数字最值钱。Opus 5.5 证完一半目标，token 比 Opus 5 少约 40%。多个 agent 共享一个证明工作区、前一个的引理后一个能直接复用时，总 token 降了 17%，34 个证明里有 30 个比单打独斗便宜。这其实是一个藏在安全论文里的多 agent 记忆结论。证明和语义都已公开在 github.com/theorem-labs/oss-verify-proofs，还附了一个帮新项目接入的 Claude skill。

放回这一周看就更有意思。PHP2Shell 说明模型已经能在互联网规模上找出可利用漏洞，微软又把一场国家级攻击和一个 agent 框架挂上了钩。常规防守思路是比对手更快找 bug。这次是另一种赌法：直接证明一整类故障不可能发生，而且由一个不吃模型话术的检查器来裁决。等证明便宜到一定程度，测试就不再是一个代码库能对自己做出的最强承诺。