Anthropic 用 Claude 自动生成代码形式化证明并验证安全性

Anthropic 与 Theorem 合作，让 Claude 为 Google OSS-Fuzz 中 123 个开源库的测试程序生成约 1.8 亿行数学证明代码，并由 Rocq 自动检查。