Claude写下1.8亿行证明，揪出万亿次模糊测试漏掉的漏洞

Anthropic前沿红队与Theorem Labs发布报告，用Claude对123个开源代码库的239个测试入口完成形式化验证，约1.8亿行Rocq证明通过机器核验，找出了谷歌OSS-Fuzz万亿次模糊测试漏掉的漏洞。方法是把测试入口改写成数学命题，要求证明64MiB内任意输入都不触发崩溃或ASan报错，证明卡住可能意味着存在Bug，Claude找到Bug后自行打补丁再继续证明；在埋入7个Bug的Rust版Python解释器测试中，随机测试漏掉5个，证明全部找出。证明做在RISC-V机器码层，Claude还自主写出x86指令集数学模型，发现x86官方文档数百处错误和少量CPU硬件Bug。Theorem测得验证速度约每两个月翻一番，首批25个库、60个入口的证明已在GitHub公开。