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

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