Anthropic红队联合Theorem Labs让Claude写出1.8亿行Rocq证明，清扫123个开源库漏洞
Claude狂写1.8亿行证明，万亿次测试漏掉的Bug，被AI一锅端
AI 导读
Anthropic前沿红队联合Theorem Labs发布报告，让Claude对123个开源代码库的239个测试入口做形式化验证，累计生成约1.8亿行通过Rocq检查器核验的数学证明。
推荐理由
原文梳理了Claude形式化验证开源代码库的规模、方法和成本测算，读者可以了解形式化验证从人命关天代码走向普通开源生态的路径。