Anthropic发布报告：Claude生成约1.8亿行Rocq证明代码，让形式化验证规模化可行

Anthropic与Theorem Labs于10月23日发布报告《大模型正让形式化软件验证在更大规模上变得可行》，Claude模型针对123个开源软件库中的239个程序入口生成约1.8亿行Rocq证明代码，发现并修复数百个Bug，包括多年未被发现的漏洞。