ARTICLE · 1247035
LLM 正让形式化软件验证在远超以往的规模上成为可能
LLM 正让形式化软件验证在远超以往的规模上成为可能
Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa AgrawalEvyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai ZeldovichNicholas Carlini, Rajashree Agrawal, Jason Gross
大多数软件都充斥着 bug，而如今 AI 已能轻松发现并利用它们。抵御网络攻击的标准防线已不再足够：我们需要能够证明代码没有 bug 的方法。形式化软件验证（formal software verification）则能提供这种保证，但历史上它需要专家投入数年心血，对大多数现实项目而言并不现实。然而，在与 Theorem 的合作中，我们表明局面已然改变：LLM 如今已能大规模产出形式化证明，让包含已证明安全保证的全新软件开发工作流成为可能。借助 Claude，我们在 100 多个真实世界的开源软件库中，于汇编代码层面（RISC-V）证明了安全性质。在撰写证明的过程中，Claude 还发现了一些尽管历经数万亿次测试运行、却多年未被察觉的 bug。随着模型能力持续进步，我们预计形式化验证将成为安全软件开发中不可或缺的一环。
引言
即便成熟、经过大量测试的软件也难免存在 bug，而 LLM 在发现这些 bug 上正越来越得心应手[1]。Linux 内核是当今测试最充分的软件之一，部署在全球数十亿台设备上，最近却披露了超过 1,000 个漏洞[2]。随着前沿模型越发擅长将看似无害的 bug 串联成危害严重的漏洞利用[3]，我们需要能在这些 bug 被实际利用之前就检测并修复它们的技术。
理想情况下，这类技术应当能找出并修补所有 bug，进而给出某种证明，表明不再有遗漏。形式化验证（formal verification）就是实现这一目标的一条路径。在形式化验证中，开发者把代码转写为数学模型，然后尝试证明它始终遵守某组明确定义的安全规则。如果证明失败，就意味着代码中可能存在违反规则的 bug，而失败的样态往往暗示 bug 可能是什么。每次消除失败原因后，再重复这一过程，最终将得到一份证明：代码中不存在任何会违反这些规则的 bug。
然而，形式化验证并非易事。证明的体量可能达到原始代码的许多倍，撰写起来既费时费力，又需要一套冷门且高度专业化的技能。例如，实现 seL4 操作系统内核只花了 2 人·年，而对它做形式化验证[4]却花了 20 人·年。正因如此，形式化验证过去只在真正的关键任务应用中具备可行性，比如空客的航电代码[5]。
但 LLM 正让这一切变得容易得多。前沿模型如今已能完全自主地为真实世界的软件产出正确性证明。为了展示这一点，我们让 Claude 在 123 个开源库上证明有价值的安全性质，其中包括证明：某些可执行产物在特定条件下永远不会崩溃。具体来说，Claude 证明了这些程序总会正常退出，不会触发内存安全错误或断言失败——对任意小于 64 MB 的输入、任意建模的 Linux 操作系统（OS）响应和内存布局，在若干假设下均成立（即程序以单线程静态链接二进制的形态、在固定内存预算下，运行在使用 Linux 操作系统的 RISC-V [1] CPU 之上）。这距离修复所有可能的 bug 仍然很远，但已比以往近得多，并为最终目标勾勒出了一条路线图。
我们正在公开发布这些证明中的一部分[6]，供所有人验证与复用，同时公开的还有 RISC-V 与操作系统语义[7]。本项目的合作方 Theorem[8] 也提出可以为其他开源项目[9]运行同一条流水线，并发布了一个 Claude 技能[10]，帮助开发者上手验证自己的代码。
形式化验证是一个方法论众多的宽广领域。下文还将介绍我们借助其他形式化验证方法，加速安全与软件开发任务的初步探索，例如：评估 zlib 压缩算法的安全性、证明一个用 Rust 编写的 Python 解释器的行为等价性，以及根除关键软件中存在多年的 bug。
形式化验证前路可期。随着模型越来越智能，撰写证明的成本正在下降。此外，随着更多代码被形式化、获得安全保证的方法日趋标准化，跨代码库复用或改写证明的能力将进一步摊薄成本。我们鼓励所有开发者用 LLM 探索形式化验证——尤其是那些此前用能力较弱的模型尝试过、发现并不奏效的人。
本文余下部分将更详细地介绍我们的形式化验证实验。
把测试变成证明
要证明某款软件是正确的，必须先说清“正确”究竟意味着什么。正确性由规约（specification，spec）定义。有些程序的预期行为有清晰的形式化描述方式。例如，PNG[11] 解码器读入一段字节序列，并（依照 RFC 2083[12]）把这些字节解码为相应的图像。但对大多数程序而言，事情没这么直白：一个文本编辑器或网页浏览器，怎样才算“正确”？难以获得全面且无歧义的规约，是在更大规模上验证软件的一大障碍。
针对我们要证明的开源库代码，我们的做法是：借助一个刻画“在 Linux 上执行任意 RISC-V 编译二进制意味着什么”的通用模型，自动把这些库既有的、可编译的测试套件转换成规约，把规则编码为“这套测试套件永远通过”。从历史上看，证明这类规约几乎不可行：要让一个证明覆盖数万条汇编指令在任意输入下的全部可能行为与交互，并逐一给出论证，其复杂度天然极高（证明也因而极其庞大）。而这正是当今 LLM 的用武之地：围绕一个明确定义的目标消化数百万行代码，恰是 LLM 极为擅长的任务。
在这个项目中，我们从模糊测试（fuzz test）起步。这类测试要求开发者在代码中写一个接收输入的入口点（entry point） [2]，凡导致崩溃的输入，都对应作者关心的 bug。随后，模糊测试器（fuzzer）——一种测试引擎——会在入口点处生成海量半随机且经变异的输入，试图找出 bug（如图 1 所示）。模糊测试器运行越久，能找到的 bug 越多。但这本质上是个暴力过程：无论尝试多少输入，都无法保证走遍每条可能的代码路径。
（▶ 图 1 为模糊测试演示视频，公众号不支持内嵌播放，可点击文末「阅读原文」观看）
模糊测试的原理：让海量生成的输入流经同一入口点，从中找出会导致崩溃的输入。输入无穷无尽，搜索因此永远无法穷尽。
为了找出模糊测试本可能暴露的所有 bug，我们把模糊测试本身变成了一条定义在编译后 RISC-V 指令之上的规约。这条规约说：对任何小于 64 MB 的输入，该模糊测试都不会崩溃[3]。只要 Claude 能证明这条规约，RISC-V 上的模糊测试便属多余——对那个入口点再做模糊测试，永远不会找到任何 bug。
我们对 Google OSS-Fuzz[13] 计划中的数百个项目做了这件事。该计划为符合资格的开源项目提供持续模糊测试。OSS-Fuzz 收录了数千个由开发者编写的入口点，它们通过崩溃来暴露代码性质被破坏的情形（例如断言失败）。OSS-Fuzz 会自动用 AddressSanitizer [4]（ASan）为 C 和 C++ 程序插桩，使程序在内存被不当访问时立即崩溃——而这类不当访问正是软件漏洞的主要成因[14]。像内存安全这样的普适规约，几乎适用于所有软件。
（▶ 上图为规约生成与证明检查流程演示视频，可点击文末「阅读原文」观看）
开源库及其既有的模糊测试被编译为 RISC-V 可执行程序。这个可执行程序，连同 Theorem 的 RISC-V 与操作系统形式化语义以及期望的“不崩溃”性质，机械地生成出一份证明必须满足的规约。Claude 撰写证明；Rocq 内核对照规约检查证明。绿色标记已证明的部分——前提是各可信组件正确无误。
短短几周内，Claude 修补了自己发现的 bug，继而证明：对 123 个不同 OSS-Fuzz 库的 239 个入口点，任何输入（最大 64 MB）都不会导致崩溃。这些证明作用在编译后的 RISC-V 指令（即可执行二进制程序）上，总计约 1.8 亿行 Rocq；典型的一份证明约 600,000 行，为其提供安全保证的二进制程序，RISC-V 指令数中位值为 18,000 条。这些证明的构建方式，是用 Theorem 的 RISC-V 指令语义与 Linux 进程语义，把 RISC-V 汇编代码翻译成数学模型。这也意味着，这些证明目前假设：程序以单线程静态链接二进制的形态、在固定内存预算下，运行在使用 Linux 操作系统的 RISC-V CPU 上。扩大这些证明的覆盖范围是完全可以做到的，只需为更多汇编架构和其他操作系统进程建立标准化语义。关于 Claude 写下的证明，可参阅专家视角[15]的评述。
（▶ 上图为形式化证明覆盖所有可达路径的演示视频，可点击文末「阅读原文」观看）
一份覆盖所有输入的形式化“不崩溃”证明，排除了从入口点可达的任何路径上的全部崩溃。在迭代证明的过程中，Claude 还能找出并修复其余任何可达的、会引发崩溃的 bug。
虽然证明代码体量巨大，但几乎完全无需人工审阅。Rocq 证明检查器会确保证明正确满足规约。因此，开发者唯一需要信任的产物只有三样：
• RISC-V 与 Linux 进程的形式化模型； • 被证明定理的准确陈述； • Rocq 证明检查器本身[5]。
这并不意味着这些库就没有 bug。它意味着，任何残留 bug 要么就在上文列出的产物之中，要么落在 Claude 证明的范围之外。加固这些仍可能藏 bug 的可信组件（Rocq、RISC-V 与 Linux 语义）并非小事，但与调试这些规模化证明所覆盖的每一行代码相比，这要好办得多——尤其考虑到这套方法无需增大可信组件，就能守护任意数量的项目。
我们欢迎对这些证明的独立验证，也鼓励对我们的方法加以改进。为此，我们将公开：本项目自制的、尚未公开的可信组件（如上）；无需修补的那些模糊测试的 Claude 完整 Rocq 证明；以及我们未能证明的其他模糊测试的规约。
发现并修复 bug
上文已经展示，许多开源库中由开发者编写的测试（模糊测试）可以转化为规约，而且有时只需先修补残留 bug，Claude 便能证明它们永远通过。也正因如此，尝试证明这些规约的过程挖出了数百个 bug。
在证明数百个入口点的过程中，大量 bug 现身。为了让 Claude 不必每次都停下来等人介入，我们让它自己修复找到的 bug：它给代码打补丁，规约随之基于打补丁后的代码重新生成，然后 Claude 继续证明新的规约[6]。
我们发现的许多 bug，是模糊测试器几乎不可能找到的。模糊测试器变异的是小输入（通常上限为 1 MB[16]），而且通常依靠代码覆盖率指引方向。在证明某个库的一个入口点时，Claude 在该库自带的一份解压器代码中发现一个计数器下溢，会引发越界写入——但只在输入约 20 MB、且具有某一种罕见而特定的布局时才触发。其他 bug 还有：一个图像解码器中的越界读取，需要 64 MB 输入和超过 2 GB 内存；另一个库中的越界读取，需要对同一文件的两个句柄发起一组特定的调用序列；以及重新发现了 libexpat 中的 CVE-2026-56132，它需要深度嵌套的输入。Claude 还找到了一些根本不会崩溃的逻辑 bug。例如，在证明某个库内存安全时，它注意到一项“限制应用可加载哪些文件”的功能并未总是生效。
本项目的终极目标，是证明经 RISC-V 编译的模糊测试再无残留崩溃可寻。但上述 bug 说明，无论这个目标是否达成，这个过程都另有一重价值：哪怕只是尝试，也会挖出必须修复的真实 bug。
证明的不止内存安全
证明一个模糊测试再无可寻的崩溃，其意义比听上去更大。现实代码中的模糊测试，常常在检验有意义的高层性质是否被违反，例如编码-解码往返一致性、幂等性、代数定律、差分测试、自洽性，或与参考实现的等价性。例如，LZO 压缩算法的一条模糊测试断言：把输入压缩再解压，结果应与原始输入相同。若性质不成立，程序就会崩溃——因此，证明测试永不崩溃，就等价于证明了性质本身。
即便性质并非由开发者直接指定，这种情况也会出现。例如，Claude 要完成 cpp-httplib 的 OSS-Fuzz 证明，就必须排除 std::set 析构函数因递归过深而栈溢出的可能。这一递归深度受树的最大深度约束，因此 Claude 必须（在机器码上！）证明 libc++ 的红黑树再平衡算法经过正确优化，能让树的深度保持对数级有界。
其他形式化验证案例
形式化验证是一片广阔的领域。上面“模糊测试变证明”的例子，是 LLM 通过把证明直接应用于机器码、让形式化验证更易普及的一个实例。
LLM 与形式化验证的结合，在其他用法上同样有所斩获。例如，我们让 Claude 为 RFC 1950[17]——定义 zlib 压缩文件格式的技术文档——撰写形式化规约；然后让 Claude 证明 Linux 内核中的 zlib 实现正确实现了该规约。与上面的例子一样，Claude 在二进制层面证明这条性质，只不过这次不是 RISC-V，而是使用 Claude 自行生成（且经过大量测试）的 x86 指令集架构（ISA）形式化语义，直接证明了 x86 编译的二进制程序[7]。此后，我们又对另外六个广泛使用的库重复了这一流程。一路下来，我们在边角情形中发现了一些轻微的（不可利用的）bug，正在向各自上游提交。从这轮实践中我们得出两个结论：（1）这些测试极其充分的代码库已经几乎完全正确；（2）对现实存在的代码库证明端到端的正确性性质，是可行的。
在另一个实验中，我们让 Claude 用 Rust 开发一个覆盖 Python 大部分子集的解释器，并（使用 Rust 验证工具 Verus）证明它遵循一篇学术论文所勾勒的 CPython 语义。随后，我们用实验度量其与 CPython 行为的一致程度：运行超过 170 万个随机生成的 Python 程序，99.95% 的测试表现与 CPython 完全一致，其余差异均为意料之中的已知边角情形。
我们还通过对简单安全性质的形式化验证，在多款广泛使用的关键应用中发现了问题。其中一项，我们发现了一个此前未知、潜伏十多年的逻辑 bug。在验证一款广泛使用的 PDF 阅读器时，我们一周内找到的安全 bug 数量，相当于通常一整年的报告量。
其中一些工作的更多细节，见附录[15]。
这只是开始
LLM 辅助形式化验证的一大关键局限，在于证明可能要耗费数亿 token 才能产出。如果目标是让整个软件生态系统都用上这些方法，成本效率就至关重要。所幸，我们有充分理由预期效率会不断改善。
更新的模型更省 token
我们用真实 OSS-Fuzz 代码[15]构建了 36 个小型验证任务。Opus 5.5 只用比 Opus 5 少约 40% 的 token，就证明了其中一半任务。随着模型在长验证任务上得到训练，我们预计这一趋势将延续。
Opus 5.5 比早先模型更快完成证明。图为在给定 token 预算下，由单个智能体证明的 36 个形式化验证任务的占比。每个任务在 5M token 预算下获得三次独立的单智能体尝试；只要第一次尝试完成，该任务即计为已证明。
证明可以复用
智能体各自为战时，常常重复大量劳动。证明和软件一样，是由更小的证明递归构建而成——证明越小，往往越容易复用。为了度量这种影响，我们让智能体在证明各自目标时可以互相拷贝证明。有了这个共享工作区，智能体所需 token 比单打独斗时减少 17%，一些此前单独尝试失败的智能体也借此取得了成功。
同一共享工作区中的 36 个证明，按完成顺序排列。弧线连接任意两个共享同一未更改文件的证明；柱条表示撰写每个证明所花的 token，黑线表示同一任务由单干智能体完成的平均成本——在 34 个已完成的证明中，有 30 个的这一成本更高（36 个证明中有两个是单干智能体未能完成的）。
在 OSS-Fuzz 证明攻坚期间，我们观察到同一现象在更大规模上重演。一份证明的大部分篇幅，处理的是所有程序都包含的代码（尤其是 C 运行时与 AddressSanitizer 的初始化），因此差异悬殊的程序，其证明也会有显著重叠。智能体团队充分利用这一点：拷贝另一支团队已完成的证明，再将其适配到自己的程序（图 6）。
智能体拷贝既有证明，并将其适配到每个新程序。每列代表一个程序的完整证明，按字节占比展示。各方块是证明的组成部分，显示其中原样保留、轻度修改（同一文件、大小相差在 2% 以内）、大幅修改或新写的比例。共享部分几乎没有增加新代码。
正是凭借这种可复用性，Mathlib[18]——Lean 中的形式化数学共享库——才增长到近 300,000 条定理[19]、由 700 多位贡献者提交：每条新证明都建立在既有成果之上。在 OSS-Fuzz 攻坚中，我们也积累了相当规模的证明库，其中一部分将随本次发布公开（可能暴露开源软件中未修补 bug 的证明，不在发布之列）。
当这些初步实验告一段落，我们需要一套验证海量既有软件的策略，并从最关键的依赖做起。正如已经展示的，这条路可以规模化：采用通用规约、在二进制层面工作，从而免去用另一种语言重写整个代码库。
这套方法还让证明能以包为粒度复用——每个依赖只需验证一次。依赖关系呈幂律分布：哪怕只证明一小批共享库，也能让一大片软件变得可证。更多细节，见 Theorem 为验证整个 Nix 生态系统制定的路线图[20]——其中包括 glibc、OpenSSL、cURL 等关键基础设施。
局限性
在实践中，形式化验证能证明的代码安全性，有时不及我们的期望。
“经过形式化验证”不等于“没有 bug”。Claude 可以写出证明，表明编译后的程序行为满足某份形式化规约的要求（该证明由外部证明检查器核验）。但证明检查器无法告诉你，规约是否与现实相符。要与现实相符，规约必须正确涵盖并建模被验证程序所运行的真实机器的一切，包括 CPU 与操作系统。已验证代码中之所以仍会出现 bug，是因为规约或所假设的机器语义与现实存在出入。好在这也意味着，我们知道该去哪里找残留 bug，也知道如何设计一个把这些潜在缺陷压到最小的系统。下面具体说明这些差距如何体现在我们的证明中，以及未来可以怎样弥合。
真实机器会做出模型未加描述的行为。我们的证明针对的是静态链接 musl libc 的单线程 RISC-V 二进制程序。但大多数人是在 x86 或 ARM 上运行这些库，并动态链接 glibc。要缩小这一差距，我们需要更贴近实际部署系统的系统模型。例如，朝此方向迈出的一步，是为 x86 生成准确的语义。
证明声明的内容，未必覆盖我们关心的一切。我们证明的是，在 Google OSS-Fuzz 的许多模糊测试入口点上，任何小于 64 MB 的输入都不会触发崩溃，包括 ASan 崩溃。然而，ASan 并检测不出所有内存安全 bug，而我们也没有验证每个库的全部入口点。即便验证了，仅凭全部入口点也覆盖不了整个库（尤其是存在死代码时）。此外，真实程序可能会错误地使用这些库，导致调用方出现内存损坏。要弥补这一差距，需要为每个公开函数规定调用方必须做到什么，而调用方也必须严格遵守。
我们预计，随着对“借 LLM 之力运用形式化方法”的认识加深、模型持续改进，这些局限将变得可以克服，我们也终将能对我们所依赖代码中大得多的比例完成验证。
结论
大势已然清晰：形式化验证在过去仅限于专家为最安全攸关的代码量身打造的保证；不久之后，它将变得像今天的模糊测试一样，对几乎所有生产软件都切实可用。正如静态类型、测试框架与其他正确性工具走过的路，验证将从“外挂式”走向“内置式”——驱动这一进程的不只是 LLM，还有语言设计与开发工作流的革新。
在 LLM 自动扫描并找出越来越多代码漏洞的今天，我们必须采用能够保证代码安全性质的流程。由 LLM 驱动的规模化形式化验证，为在以往无法企及的范围与规模上获得这些保证，提供了一条大有前景的路径。我们鼓励更多同行动手实验，携手建成这样一个世界：健壮的软件广泛普及，软件 bug 则成为人们了如指掌、可迅速处置的罕见之物。
阅读完整附录。[15]
注释
[1] RISC-V 是一种处理器设计，与 x86 或 ARM 类似，它定义了软件最终被编译成的汇编指令——即芯片执行的基本命令。
[2] 入口点是代码作者为测试而开的一扇“前门”。任何传入入口点并导致崩溃的输入，都对应作者关心的 bug。
[3] 调高这一上限只需极少的人工：改一下参数、重新生成规约，再让 Claude 重新证明该命题。
[4] AddressSanitizer 是一种编译器工具，它为程序加入检查，使缓冲区溢出、释放后使用等内存错误在运行时一发生就被检测并报告出来。
[5] 严格说来，这也意味着我们还必须信任 Rocq 证明检查器所依赖的硬件、操作系统和 OCaml 编译器。
[6] 需要注意，这给奖励作弊（reward hacking）留下了空间。奖励作弊指 AI 模型找到一条捷径，从技术上达成了给定目标，却没有做实际想让它做的事——好比一个学生靠背答案通过考试，而不是学会知识。在本场景中，Claude 可以把程序改写成一个“平凡地永不崩溃”的程序，从而让任何定理都可证。为了遏制这种做法，我们对任何补丁都施加惩罚，并为证明“补丁改变了哪些输入、这些输入多么少”提供额外加分。我们还对这些补丁记录日志并审计，以排查上述失败模式。
[7] 我们认为，Claude 能够完全自主地生成一套指令集架构（ISA）的形式化语义，这一点本身就是另一个有趣的启示。虽然我们无法确信这套语义本身完美无缺，但经验表明，逐条单步执行我们的语义，足以在 Linux 内核之上启动一个 Ubuntu 用户空间。生成这套语义的过程中，还在官方参考文档中发现了数百处错误，并在硬件本身发现了数量较少的一些 bug。
引用链接
[1] 越来越得心应手: https://hacks.mozilla.org/2026/05/behind-the-scenes-hardening-firefox/[2] 超过 1,000 个漏洞: https://lwn.net/Articles/1097401/[3] 将看似无害的 bug 串联成危害严重的漏洞利用: https://www.anthropic.com/research/exploit-evals[4] 对它做形式化验证: https://sel4.systems/Research/pdfs/comprehensive-formal-verification-os-microkernel.pdf[5] 空客的航电代码: https://www.astree.ens.fr/papers/astree_airbus_sas2007.pdf[6] 这些证明中的一部分: https://github.com/theorem-labs/oss-verify-proofs[7] RISC-V 与操作系统语义: https://github.com/theorem-labs/rocq-linux-process-semantics[8] Theorem: https://theorem.dev/[9] 其他开源项目: https://theorem.dev/oss-verify/[10] Claude 技能: https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md[11] PNG: https://en.wikipedia.org/wiki/PNG[12] RFC 2083: https://www.rfc-editor.org/info/rfc2083[13] OSS-Fuzz: https://github.com/google/oss-fuzz[14] 软件漏洞的主要成因: https://www.cisa.gov/news-events/news/cisa-nsa-fbi-and-international-cybersecurity-authorities-publish-guide-case-memory-safe-roadmaps[15] 专家视角: https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf[16] 通常上限为 1 MB: https://github.com/AFLplusplus/AFLplusplus/blob/stable/include/config.h#L314[17] RFC 1950: https://www.rfc-editor.org/info/rfc1950/[18] Mathlib: https://leanprover-community.github.io/[19] 300,000 条定理: https://leanprover-community.github.io/mathlib_stats.html[20] 路线图: https://theorem.dev/blog/verified-software-stack/
