利用 Claude 大规模对软件进行形式化验证

Anthropic与Theorem团队用Claude在几周内写出了约1.8亿行通过机器核验的Rocq形式化证明，对Google OSS-Fuzz里的123个主流开源库（共239个测试入口，涵盖cJSON、OpenSSL、zstd、simdjson等）做了汇编级安全验证。相比传统模糊测试（Fuzzing）靠随机喂数据“碰运气找崩溃”，形式化验证能穷尽特定范围内的输入路径，顺藤摸瓜揪出潜伏多年的深层漏洞。但先别把这当成“这123个库已经绝对零Bug”——拆开官方技术附录与开源仓库，它的真实含金量与严苛边界非常分明。

为什么能揪出模糊测试跑几年都撞不到的深层漏洞
传统模糊测试一般把测试输入限制在1MB左右，靠代码覆盖率引导搜索；而Claude在推导数学证明时，只要有一条极端分支证不通，就顺藤摸瓜定位出了潜伏多年的真漏洞。比如某解压库里一个计数器下溢引发的越界写，只有在约20MB且特定罕见布局的输入下才会触发；某图像解码器的越界读需要整整64MB输入和超2GB内存；它还在libexpat中独立重现了嵌套过深触发的CVE-2026-56132，甚至揪出了“文件加载限制未生效”这类根本不会引发崩溃的逻辑缺陷。
不过要注意两点：第一，为避免暴露尚未公开修补的漏洞，官方目前在GitHub（oss-verify-proofs）上实际公开供外界核验的只有无需打补丁的25个库、60个测试入口；第二，遇到证不通的漏洞时，研究允许Claude自动打补丁再继续证明——虽然设置了惩罚项防止模型把程序粗暴改成“直接退出以规避崩溃”，但123个库里到底有多少是先打了补丁才证出来的，官方并未披露比例。

1.8亿行证明是怎么写出来的：九成篇幅在证底层环境
一个仅391行C代码的cJSON解析入口，Claude写出的证明竟高达63万行（单份证明普遍在33万到90万行之间，CPU核验一次就要跑30分钟到数小时）。为什么这么庞大？因为形式化证明直接针对编译后的RISC-V机器码，必须把C语言启动过程、内存分配器、printf以及AddressSanitizer（超10万条指令）的运行时从头到尾全部证一遍——cJSON那63万行证明里，只有约十分之一真正和cJSON自身业务代码有关，而且超过一半篇幅是Claude自己写脚本生成的指令编码与查找表。
也正因底层运行时高度雷同，后续开源库可以直接把前一个库证好的底层部分复制过来微调。在libcups、freerdp和libzmq三份完整证明的对比中，后两个库在内存分配器、Sanitizer运行时和共享库部分完全没有新建目录，全靠复用前人成果；