Anthropic 用 Claude 完成 123 个开源库形式化验证，狂写 1.8 亿行 Rocq 证明

Anthropic 前沿红队与 Theorem Labs 让 Claude 对 123 个开源代码库的 239 个测试入口完成形式化验证，累计写出约 10 亿行 Rocq 证明，其中约 1.8 亿行通过机器核验。过程中揪出了谷歌 OSS-Fuzz 上万亿次模糊测试未触及的漏洞，还发现 x86 官方文档数百处错误及少量 CPU 硬件缺陷。首批 25 个库、60 个入口的证明已在 GitHub 公开。