Anthropic 让 Claude 自动为代码生成形式化证明

Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 对 Google OSS-Fuzz 项目中 123 个开源库的测试程序做形式化验证，几周内生成约 1.8 亿行数学证明代码，由独立验证程序 Rocq 自动检查，Anthropic 称过程几乎不需要人工审阅。Claude 并未编写新代码，而是把崩溃测试转成数学问题、分析编译后的机器码并产出证明，期间发现数百个 bug 并自行修复，其中包括一个十余年未被发现的逻辑错误；在验证一款常用 PDF 阅读器时，一周内发现的安全漏洞数量相当于该软件通常一整年的报告量。