Anthropic 用 Claude 为现有代码自动生成形式化证明并查出漏洞

Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 把现有代码转成数学证明：几周内生成约 1.8 亿行证明代码，覆盖 Google OSS-Fuzz 项目中 123 个开源库的测试程序，并由独立的验证程序 Rocq 自动检查。