Claude狂写1.8亿行证明！万亿次测试漏掉的Bug，被AI一锅端
2026.10.24 · 事件 · AI事件 · 媒体报道
Anthropic让Claude对123个开源库做形式化验证，写出1.8亿行通过机器核验的证明。
Anthropic前沿红队联手Theorem Labs，让Claude对123个开源代码库的239个测试入口做形式化验证，累计写出约10亿行Rocq证明，其中约1.8亿行通过检查器核验。过程中揪出模糊测试上万亿次都没撞出的漏洞，还发现x86官方文档数百处错误和少量CPU硬件Bug。
- Claude完成123个开源库239个入口的形式化验证
- 累计写约10亿行证明，1.8亿行通过Rocq检查器
- cJSON仅391行C代码，对应63万行证明
- 发现x86文档数百处错误及少量CPU硬件Bug
- 验证速度约每两个月翻一番，证明可复用省17%token
为什么值得看
形式化验证从只有空客飞控用得起，变成几周覆盖上百个开源库。
适合谁关注
关注AI编程、软件安全与形式化验证的开发者。