AI 写代码已经不稀奇，AI 证明代码不崩溃才吓人。Anthropic 拉上 Theorem，让 Claude 给 123 个开源库的 239 个 OSS-Fuzz 入口做形式化验证，结论是：在特定条件下，这些入口不会崩溃。
注意是「证明」，不是「测了很多遍没炸」。覆盖范围是小于 64MB 的任意输入，跑在 Linux 上固定内存预算的单线程静态 RISC-V 二进制。换句话说，它证明的是一个非常窄、但非常硬的命题，不是「这库没 bug」。
证明代码写了约 1.8 亿行 Rocq，由外部检查器验证，开发者要信任的只剩机器语义模型、定理陈述和检查器本身。
最有意思的是，Claude 在证明过程中挖出了长期没被模糊测试抓到的缺陷，顺手修了。模糊测试跑了那么久没发现，形式化验证一上来就撞见，这就是「测试没发现错误」和「数学上证明不发生」的差距。
但别急着高潮，研究自己划了边界：不是每个库的全部入口都验证了，证明不等于整个库 bug-free。团队公开了部分证明、RISC-V 和 Linux 语义、入门 skill，但没公开可能暴露未修补漏洞的那部分。这个克制是对的，工具链成熟之前，公开等于给攻击者递刀。
真正值得兴奋的不是「AI 消灭漏洞」这种标题，而是从「跑一万次没炸」到「在给定条件下数学证明不炸」这一步跨出去了。软件安全终于开始有点像工程，而不是玄学。
正文完