Claude 生成 1.8 亿行验证代码，挖出万亿次测试遗漏漏洞

Anthropic 联手 Theorem Labs 借助 Claude 开展数学级软件漏洞清扫，让 Claude 深入底层 RISC-V 汇编指令对大量生产级开源代码库做形式化验证，数周内完成 123 个开源代码库中 239 个测试入口的形式化验证，生成 1.8 亿行通过核验的 Rocq 数学证明代码，挖出了此前模糊测试跑上万亿次都没发现的隐秘漏洞、潜伏十余年的高危逻辑死角，甚至 x86 处理器硬件缺陷与官方文档错误。该方法将测试入口转化为数学命题完成全路径全输入的覆盖证明，一旦证明卡住就可能定位漏洞，还能自动完成补丁修复后继续验证，相比传统随机测试漏检率大幅降低。这类底层到机器码的形式化验证过去工程量极高，如今依托大模型能力验证效率飞速提升，验证速度约每两个月翻一番，证明内容还可跨项目复用，按当前趋势推算投入约 1.34 亿美元到 2027 年底有望完成 Nix 生态 95% 机器码的验证，目前首批相关证明已公开，为当前日益严峻的网络安全形势提供了新的解决路径。