Anthropic发布重磅报告：Claude狂写1.8亿行证明代码，横扫传统测试遗漏的底层漏洞

全球软件行业正面临严峻挑战，短短48小时内爆发27起重大网络攻击，「最暗十月」的危机迫在眉睫。在此背景下，Anthropic前沿红队团队与Theorem Labs联合发布了一份重量级报告，展示了一种全新的安全保障方案：让AI模型Claude深入到底层汇编指令进行形式化验证。

报告显示，在短短几周内，Claude对123个开源代码库中的239个测试入口进行了形式化验证，狂写了约1.8亿行Rocq数学证明代码并全部通过机器核验。在这场针对底层代码的清扫中，那些万亿次模糊测试未能发现的隐秘漏洞、潜伏十余年的高危逻辑死角，乃至x86处理器硬件本身的真实缺陷悉数现形。

与传统依赖运气的模糊测试不同，Claude将测试转化为数学命题，证明在特定条件下小于64MiB的任意输入都不会触发崩溃。例如在一个热门PDF阅读器中，Claude一周挖掘的安全漏洞数量等同于其通常一整年的报告量；在故意埋下7个Bug的Python解释器测试中，随机测试仅放行5个，而形式化验证一个都没放过。

为了达到机器码层面的绝对严谨，Theorem团队建立了RISC-V指令和Linux进程的数学模型。以JSON解析库cJSON为例，其源代码仅有391行C代码，但Claude为其及相关运行时环境生成的证明代码膨胀至63万行。整个项目中Claude累计撰写了约10亿行证明代码，其中近一半由AI自生工具自动完成，最终约1.8亿行通过了Rocq检查器的严格验算。

验证能力不仅限于软件层面，Claude还自主构建了x86指令集的数学模型，实现了从Linux内核启动到CPU指令推演的完整验证。在此过程中，AI找出了x86官方参考文档中的数百处错误，并发现少量隐藏在CPU硬件本身的Bug。Anthropic预测，若验证速度保持每月翻倍且每年投入1亿美元，到2027年底有望将Nix生态95%的机器码纳入证明覆盖。