Claude给123个开源库写出1.8亿行数学证明，找出数百个Bug

BiRun 讯，Anthropic 联合形式化验证公司 Theorem，让 Claude 用数学方法检查软件漏洞。传统测试通常靠不断输入随机数据，看看程序会不会崩溃。但无论测试多少次，都无法保证没有遗漏。这次 Claude 直接为程序编写数学证明，试图从根本上排除特定类型的错误。

几周内，Claude 为 123 个开源库的 239 个测试入口完成验证，生成约 1.8 亿行证明代码，并交给 Rocq 数学证明工具检查。结果表明，在指定运行环境下，这些程序面对小于 64 MB 的任意输入，都不会触发测试所检查的崩溃。

证明过程中，Claude 还发现并修复了数百个 Bug。比如，一段解压程序只有遇到约 20 MB、结构极其特殊的数据，才会发生内存越界写入。另一处图像解码漏洞需要 64 MB 输入和超过 2 GB 内存才能触发。常规随机测试很难碰到这些情况。

这类数学验证过去极其费时。比如 seL4 操作系统内核，开发累计投入约 2 年的全职人力，数学验证却需要约 20 年，是开发工作量的 10 倍。

信源

动察 Beating 频道 · 动察 Beating 交流群。