Anthropic 用 Claude 自动生成形式化证明验证现有代码

Anthropic 与 Theorem 让 Claude 自动为现有软件生成形式化证明，验证其在限定条件下是否正确。Claude 在几周内生成约 180 million 行数学证明代码，测试程序取自 Google OSS-Fuzz 项目的 123 个开源库，Rocq 会自动检查证明。