Anthropic 让 Claude 对开源库做汇编层形式化验证，产出约 1.8 亿行证明代码

Anthropic 与 Theorem 合作，让 Claude 在几周内为 123 个开源库中的 239 个测试入口完成形式化验证，产出约 1.8 亿行通过机器检查的证明代码。团队称这是其所知首次在汇编代码层面对生产软件开展大规模形式化验证。具体做法是让 Claude 证明规定范围内的所有输入都不会触发约定错误，证明过程反过来帮助它找出漏洞，例如在一个解压器中发现需要约 20MB、排列特殊的输入才会触发的越界写入，而常规模糊测试通常把输入限制在 1MB 以内；团队称由此已发现数百个 Bug。在 cJSON 库中，一个 391 行 C 代码的解析入口对应约 63 万行证明，其中超过一半由 Claude 自己写的工具自动生成，最终交由人类开发的 Rocq 证明检查器验算。团队已公开 25 个库、60 个测试入口的证明供开发者下载复用。