Anthropic 与 Theorem Labs 报告：大模型正让形式化软件验证在更大规模上变得可行

Anthropic 与 Theorem Labs 团队利用 Claude 模型生成约 1.8 亿行 Rocq 证明代码，对 123 个开源软件库中的 239 个程序入口进行形式化验证，并发现修复了数百个 Bug，其中包括曾历经数万亿次测试未被发现的漏洞。