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

21 小时前

Anthropic与Theorem Labs合作，利用Claude模型对底层RISC-V汇编指令进行深入分析，对大量生产级开源代码库开展形式化验证。在数周内，完成了123个开源代码库中239个测试入口的验证工作，生成了1.8亿行通过核验的Rocq数学证明代码。这一过程中，发现了此前模糊测试未能察觉的隐秘漏洞、潜伏多年的高危逻辑问题，甚至揭示了x86处理器硬件缺陷及官方文档错误。该方法通过将测试入口转化为数学命题，实现了全路径全输入的覆盖证明，一旦证明受阻，即可定位漏洞，并自动进行补丁修复后继续验证，显著降低了漏检率。过去，这类从底层到机器码的形式化验证工程浩大，如今借助大模型能力，验证效率大幅提升，速度约每两个月翻一番，且证明内容可跨项目复用。据预测，投入约1.34亿美元，到2027年底有望完成Nix生态95%机器码的验证。目前，首批相关证明已公开，为网络安全领域提供了新的解决思路。