从“测不出来”到“证明没有”：大模型把形式化验证拉进了现实

过去一年，AI 最让安全圈紧张的能力是“找漏洞”。本周两条新闻把话题推进了一步：OpenAI 公布了用前沿模型发现 PHP 严重漏洞后的全球协同响应框架（Patch the Planet）；Anthropic 与验证初创公司 Theorem 则发表研究，称让 Claude 在 123 个开源库上写出了机器可检查的安全证明。前者说明“找洞”已经快过“补洞”，后者尝试回答：能不能干脆证明代码里没有这类洞？

一、为什么模糊测试不够了

模糊测试（fuzzing）是向程序入口喷射海量半随机输入，看会不会崩溃。它是暴力搜索，跑得再久也无法保证覆盖所有路径。Anthropic 的文章给了几个例子：某解压库里的计数器下溢，只有约 20 MB 且布局特殊的输入才触发；某图像解码器的越界读取需要 64 MB 输入和超过 2 GB 内存。而主流模糊器的输入通常被限制在 1 MB 左右，这类漏洞几乎不可能被撞到。当攻击方也用模型做漏洞挖掘时，“多测一点”就不再是可靠防线。

二、核心思路：把现成的测试变成规格

形式化验证的传统瓶颈有两个：一是证明比代码长得多（seL4 内核实现用了 2 人年，验证用了 20 人年），二是“正确”本身难以定义。

这项工作绕开了第二个难题：直接把开发者已有的模糊测试入口变成规格——“对任何小于 64 MB 的输入都不崩溃”。库连同测试被编译成 RISC-V 可执行文件，再借助 Theorem 提供的 RISC-V 指令集与 Linux 进程形式语义，机械地生成待证命题；Claude 负责写证明，Rocq 证明检查器负责判定对错。

数字上：几周内，Claude 先修补它发现的 bug，再为 123 个 OSS-Fuzz 库的 239 个入口证明了无崩溃，总量约 1.8 亿行 Rocq，单个证明约 60 万行，对象是中位数约 1.8 万条指令的二进制。这些证明几乎不需要人工审阅，需要信任的只有三样：RISC-V/Linux 的形式模型、定理陈述本身、证明检查器。

三、顺带的收获：证明失败即漏洞

证明过程本身就是漏洞探测器：证不下去，往往意味着真有 bug。文章称这一过程发现了数百个 bug，包括重新发现 libexpat 的 CVE-2026-56132，以及一个“限制可加载文件”的功能并不总被强制执行的逻辑缺陷。

另一个细节是“奖励作弊”：既然允许模型改代码，它理论上可以把程序改成“永远不崩溃的空壳”让定理好证。研究者的对策是惩罚补丁，并对“改动了哪些输入、改动多小”给予额外奖励，同时记录并审计所有补丁。

成本也在改善：在 36 个小型验证任务上，Opus 5.5 解出一半任务所用 token 比 Opus 5 少约 40%；让多个智能体共享工作区、互相复制证明，可再省约 17%。（以上均为 Anthropic 自测。）

四、别把“已验证”读成“没有 bug”

• 模型与现实的差距：证明针对单线程、静态链接 musl libc 的 RISC-V 二进制，而多数人跑的是 x86/ARM、动态链接 glibc。
• 命题覆盖有限：证明的是 ASan 能检测到的崩溃；ASan 并非覆盖所有内存安全问题，也没有验证每个入口，调用方误用库造成的内存破坏同样不在范围内。
• 代价仍高：单个证明可能耗费数亿 token。

bug 没有消失，只是被压缩进了一小撮可审计的“可信基”里——这正是形式化验证的价值所在。

这意味着什么

1. 攻防不对称正在被重新定价。 OpenAI 同一周也把“形式化验证”列为构建更安全软件底座的方向之一。模型能批量找洞时，防御端需要的是“可证明的下界”，而不是更长的测试时间。
2. 验证的瓶颈从“人力”转向“规格”和“可信基”。 用现有测试当规格、在二进制层面工作，是务实路线：不必重写代码库，依赖项只需验证一次，证明还能复用。
3. 保持清醒。 这是厂商自己的研究，证明范围受限于模型假设。真正的检验是第三方复核：部分证明已公开在 GitHub。对开发者而言，值得现在做的是给模糊测试写更有意义的断言（往返一致性、幂等性等），它们正是未来可被“证明”的规格。

参考资料

• Anthropic Research：LLMs are making formal software verification feasible at a much larger scale（2026-10-22）— anthropic.com/research/formal-v…
• OpenAI：Patch the Planet（2026-10-21）— openai.com/index/coordinated-di…
• GitHub：theorem-labs/oss-verify-proofs — github.com/theorem-labs/oss-ver…
• AI Compass 2026-10-22 日报 — ashutoshai.com/ai-compass