Claude给123个开源库做形式化证明

测试跑得再多，也不能保证软件没有 bug。Anthropic 10月22日发布与验证创企Theorem的合作研究：用Claude为123个真实开源库写出了形式化安全证明——从数学上论证这些程序在任何输入下都不会触发内存越权或断言失败。按官方说法，这是首次用AI在汇编代码层面大规模验证生产级软件。

形式化验证的思路，是把代码翻译成数学模型，然后证明它永远满足一组安全规则。这套方法最可靠，但也最贵：证明往往比原代码大好几倍，写证明又需要极小众的专业技能。seL4操作系统内核用了两人年实现，形式化验证却花了二十人年，因此过去只有空客航电这类要命场景才用得起。

Anthropic的切入点相当聪明：不给每个程序从头写规格，而是把开源库现成的模糊测试（fuzz test）自动转成规格——规则只有一条，"这套测试永远通过"，再配上一个描述任意RISC-V二进制程序在Linux上执行行为的通用模型。至于在数万条汇编指令、所有可能输入下完成论证这种庞杂活，恰恰是大模型擅长的：从123个库里的数百个入口函数开始，让Claude自行产出证明，再交由外部证明检查器核验。

真正的意外收获是挖 bug。证明失败本身就在提示"这里有猫腻"：整个过程发现了数百个问题，其中不少是模糊测试几乎不可能碰到的。fuzzer的输入通常封顶1MB，而Claude发现某个解压库的计数器下溢会导致越界写入——但只在约20MB、且布局极其特殊的输入上触发；另一个图像解码器的越界读需要64MB输入加2GB以上内存才会现形；它还顺手重新发现了libexpat里需要深度嵌套输入才触发的CVE-2026-56132。官方的说法是，这些 bug 在数万亿次测试运行下都逃了多年。而且Claude不用等人类接手：自己打补丁、重新生成规格、继续证明，一条龙走完。

连指令集本身都被顺带验证了一遍。Claude自主生成了RISC-V指令集的形式化语义，靠单步执行这套语义能在Linux内核上启动Ubuntu用户态；过程中还查出官方参考手册里的数百处错误，以及少量硬件自身的 bug。

当然，"形式化验证"不等于"没有 bug"。Anthropic坦承这次证明覆盖的是单线程、静态链接musl库的RISC-V二进制，而多数人实际跑在x86或ARM加glibc的环境里；规格与真实机器之间的缝隙，就是残余 bug 的藏身处——但好处是，至少知道该去哪找了。

这项工作更现实的信号在于成本曲线：过去二十年才做得完的验证量，现在一个模型几周就能啃下来。Theorem已经放出路线图，要对整个Nix生态——包括glibc、OpenSSL、cURL这些关键基础设施——做全量验证。安全行业的下一步竞争，可能从"谁找 bug 快"变成"谁能给出证明"。