Anthropic 借助 Claude 自动验证现有代码正确性

Anthropic 与 Theorem 合作，让 Claude 为 Google OSS-Fuzz 项目中 123 个开源库的测试程序生成形式化证明。Claude 在数周内产出约 1.8 亿行数学证明代码，并由 Rocq 自动检查，过程中发现数百个漏洞，包括 PDF 阅读器一周内发现的漏洞数量通常相当于其一年上报规模。