Anthropic 联手 Theorem Labs，把 Claude 推进了一场精细到机器码级别的软件漏洞大清剿。它们让 Claude 沉到最底层，对着 RISC-V 汇编指令，给大量生产级开源代码库做形式化验证——在短短数周内，就啃完了123个开源代码库、239个测试入口，产出了1.8亿行通过核验的 Rocq 数学证明代码。
真正让人后背发凉的，是它挖出来的东西。那些模糊测试（fuzzing）跑上万亿次都没能撞见的隐秘漏洞、潜伏了十余年的高危逻辑死角，甚至 x86处理器层面的硬件缺陷和官方文档里的错误，被 Claude 一口气揪了出来。传统随机测试像拿沙子一遍遍筛漏洞，总有漏网之鱼;这套方法的狠处在于，它把测试入口直接转译成数学命题，对全路径、全输入做覆盖式证明——一旦证明在某处"卡住"推不下去，那里往往就是漏洞的藏身点，而且 Claude 还能顺手把补丁修好、再接着验证下去，漏检率被大幅压低。
放到成本尺度上看，这件事的意义更清晰。底层到机器码的形式化验证，过去是出了名的高工程量苦活，如今借着大模型的能力，验证效率正以约每两个月翻一番的速度飞涨，而且写出来的证明还能跨项目复用。按当前趋势推算，投入约1.34亿美元，到2027年底就有望完成 Nix 生态95% 机器码的验证;目前首批相关证明已经公开。当网络安全形势日益吃紧，这种"用 AI 把代码正确性变成数学定理"的路径，给行业提供了一道全新的防线。
