LLM 推动形式化软件验证大规模落地
第一章：引言
Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
大多数软件都充满漏洞，而 AI 如今已能轻易发现并利用这些漏洞。传统的网络攻击防御手段已不再足够，我们需要能够证明代码无漏洞的方法。形式化软件验证（formal software verification）本可提供这种保证，但历史上这需要专家耗费数年心血，使其在大多数实际项目中难以应用。然而，在与Theorem的合作中，我们证明了情况已发生巨变：LLM 如今能够大规模生成形式化证明，从而支持包含已证明安全保证的全新软件开发工作流。使用 Claude，我们在 100 多个真实世界开源软件库的汇编代码层面（RISC-V）证明了安全性属性。据我们所知，这是首次利用 AI 在汇编代码层面将形式化验证应用于生产级软件的大规模实践。在编写证明的过程中，Claude 还发现了那些即使经过数万亿次测试运行也未被发现的、隐藏多年的漏洞。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发的核心环节。
引言
即便是经过严格测试的成熟软件也难免存在漏洞，且 LLM 在发现这些漏洞方面正变得愈发娴熟。Linux 内核是全球部署最广泛、测试最充分的软件之一，覆盖数十亿台设备，但近期却曝出超过 1,000 个漏洞。随着前沿模型越来越善于将看似无害的漏洞串联成关键利用手段，我们必须能在漏洞被现实利用之前检测并修复它们。
理想情况下，这类技术能够找出并修复所有 bug，进而证明不存在更多问题。形式化验证（Formal verification）是实现这一目标的方法之一。开发者将代码转换为数学模型，然后尝试证明其始终遵循一套预定义的安全规则。如果无法完成证明，则意味着代码中可能存在违反规则的 bug，而证明失败的方式往往暗示了该 bug 的特征。反复执行这一流程（每次消除导致失败的原因后），最终将得出代码不包含任何违反这些规则的 bug 的证明。
然而，形式化验证并不简单。证明过程的规模往往是原始代码的数倍，编写证明需要大量精力及小众且高度专业化的技能。例如，实现 seL4 操作系统内核花费了两个人年，但对其进行形式化验证却耗资 20 个人年。因此，形式化验证目前仅适用于真正关键的场景，如空客（Airbus）的航空电子代码。
但 LLMs 正在让这一过程变得容易得多。前沿模型现在已经能够完全自主地为真实软件生成正确性证明。为了展示这一点，我们要求 Claude 对 123 个开源库验证有用的安全属性，包括证明在特定条件下，部分可执行产物永远不会崩溃。具体而言，在某些假设下（即程序以单线程静态二进制文件形式在运行 Linux OS 的 RISC-V1 CPU 上运行，且拥有固定内存预算），Claude 证明了对于这些程序：对于所有小于 64 MB 的输入，以及每种模拟的 Linux 操作系统响应和内存布局，它们都会正常退出，不会触发内存安全错误或断言失败。这距离修复所有可能的 bug 仍有很大差距，但相比过去已迈出更大一步，并为此目标提供了路线图。
我们正在发布其中一部分证明的子集，以及 RISC-V 和操作系统语义，供任何人验证和复用。本项目的合作方 Theorem 也愿意为其他开源项目运行同样的流水线，并发布了一个 Claude skill，帮助开发者上手验证自己的代码。 形式化验证是一个方法众多的广泛领域。下面我们还会介绍一些初步探索：用其他形式化验证方法来加速安全或软件开发任务，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器的行为等价性，以及挖出关键软件中存在多年的 bug。 形式化验证的前景值得期待。随着模型越来越聪明，编写证明的成本在不断下降。而且，随着越来越多的代码被形式化、达成安全保证的方法日趋标准化，跨代码库复用或修改证明的能力将进一步摊薄成本。我们鼓励所有开发者尝试用 LLM 做形式化验证——尤其是那些以前用较弱模型尝试过、觉得行不通的人。 在本文的后续部分，我们会更详细地介绍这些形式化验证实验。把测试变成证明
要证明一段软件是正确的，首先必须说清楚"正确"到底指什么。正确性由规格说明（specification，简称 spec）定义。有些程序有明确的方式来形式化描述其预期行为。例如，一个 PNG 解码器接收一段字节序列，然后（依照 RFC 2083）把这些字节解码成对应的图像。但对大多数程序来说，事情没这么简单：一个文本编辑器或网页浏览器"正确"意味着什么？如何获得一份全面且无歧义的规格说明，是大规模验证软件的一大障碍。 针对我们在开源库中待验证的代码，采取的方法是将现有的可编译测试套件自动转换为规格（spec），通过编码“该测试套件始终通过”这一规则，并利用通用模型描述在 Linux 环境下执行任意 RISC-V 编译二进制文件的具体含义。历史上，证明此类规格几乎不可能实现。这是因为编写一个能够涵盖并对所有可能的行为和交互进行推理的证明，其内在复杂性极高——需要处理数万个汇编指令在任意输入下的表现（且由此产生的证明通常体量巨大）。这正是当今大语言模型（LLLMs）的用武之地：在数百万行代码中处理代码，以追求一个明确定义的目标，这是 LLMs 极其擅长的任务。 在这个项目中，我们是从模糊测试（fuzz tests）起步的。在这类测试中，开发者在代码中编写一个入口点（entry point）2用于接收输入；任何导致程序崩溃的输入都视为开发者关心的 Bug。随后，fuzzer（模糊测试器）——即测试引擎——会在该入口点生成海量的半随机和变异输入，试图发现 Bug（图 1 展示了这一过程）。模糊测试器运行时间越长，能发现的 Bug 就越多。但这本质上是一个暴力搜索过程，无论尝试多少输入，都无法保证覆盖所有可能的代码路径。我们在 Google 的 OSS-Fuzz 项目中实现了这一流程。该项目为符合条件的开源项目提供持续模糊测试。OSS-Fuzz 包含数千个由开发者编写的入口点，通过引发崩溃（例如断言失败）来检测代码属性错误。OSS-Fuzz 自动使用 AddressSanitizer4（ASan）为 C 和 C++ 程序进行插桩，使它们在内存访问异常时立即崩溃（这是软件漏洞的主要成因之一）。像内存安全这种广谱规范几乎适用于所有软件。
在短短几周内，Claude 成功修复了它发现的 bug，并证明了在 123 个不同 OSS-Fuzz 库的 239 个入口点上，对于任何输入（最高 64 MB）都不会发生崩溃。这些证明作用于编译后的 RISC-V 指令（即可执行二进制文件），总共包含约 1.8 亿行 Rocq 代码，典型的证明约有 60 万行，旨在为长度中位数为 1.8 万条 RISC-V 指令的二进制文件提供安全保证。这些证明通过结合 Theorem 的 RISC-V 指令和 Linux 进程语义，将 RISC-V 汇编代码转化为数学模型来构建。这意味着目前这些证明假设程序是在使用 Linux 操作系统的 RISC-V CPU 上运行的单线程静态二进制文件，且拥有固定的内存预算。扩大这些证明的适用范围是完全可行的，这只需标准化更多汇编架构和其他操作系统进程的形式语义即可。请参见对 Claude 所写证明的专家解读。
虽然证明代码数量庞大，但几乎都不需要人工审查。Rocq 证明检查器会验证证明是否正确满足规约。因此，开发者唯一需要信任的产物只有：
- RISC-V 和 Linux 进程的形式化模型；
- 被证明的定理的精确表述；
- Rocq 证明检查器本身。5
这并不意味着这些库没有 bug。它只是说明，任何残留的 bug 要么存在于上述受信产物之中，要么超出了 Claude 证明的覆盖范围。加固这些仍可能有 bug 的受信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但相比调试被大规模证明覆盖的每一行代码，这要容易处理得多——更何况这种方式可以保护任意数量的项目，而无需扩大受信组件的规模。
我们欢迎对这些证明的独立验证，也欢迎对本方法的改进。为此，我们将公开本项目中尚未开源的受信组件（如上所列）；Claude 为无需修补的 fuzz 测试生成的完整 Rocq 证明；以及我们尚未能证明的其他 fuzz 测试的规约。
发现并修复 bug
上文已经说明，你可以把许多开源库中开发者编写的测试（fuzz 测试）转化为 Claude 能够证明恒成立的规约，有时需要先修复它发现的遗留 bug。也正因如此，在尝试证明这些规约的过程中发现了数百个 bug。
Claude 在尝试证明数百个入口点的过程中，暴露出了大量 bug。为了让 Claude 不必每次都停下来等人处理，我们允许它自行修复发现的 bug：它先修补代码，这会让系统基于修补后的代码重新生成规约，然后 Claude 继续证明新的规约。6
我们发现的大多数 bug，是模糊测试（fuzzing）工具很难触及的。这类工具通过变异微小的输入来工作，通常限制在 1 MB 以内，并依赖代码覆盖率来指引其逼近缺陷。在为一个库的入口点做证明时，Claude 发现了其内置解压缩器中一个计数器下溢问题，该问题会导致越界写，但仅在约 20 MB 大小且布局极其罕见且特定的输入下才会触发。其他例子包括：一个图像解码器中的越界读，需要 64 MB 输入和超过 2 GB 内存；另一个库中涉及对同一文件两个句柄执行特定调用序列才能触发的越界读；以及对 libexpat 中 CVE-2026-56132 的再次发现，该漏洞需要深度嵌套的输入。Claude 还发现了根本不会导致崩溃的逻辑错误。例如，在证明某个库内存安全的过程中，它注意到限制应用可加载文件的功能并非总能被强制执行。
这个项目的终极目标，是达成 RISC-V 编译模糊测试不存在剩余崩溃的证明。但上述 bug 表明，无论是否达成该目标，这一流程本身都有另一重价值：仅仅是尝试执行这一流程，就能挖出真实且必须修复的 bug。
证明超越内存安全
证明模糊测试没有更多崩溃可找，其意义比表面看起来更大。现实代码中的模糊测试常常用于验证有意义的高层性质，如编码-解码往返一致性、幂等性、代数律、差异测试、自一致性，或与参考实现的等价性。例如，针对 LZO 压缩算法的模糊测试会断言：如果先压缩一个输入再解压，结果应与原始输入相同。若该性质不成立，程序会崩溃——因此证明测试永不崩溃，等价于证明该性质本身。
即便开发者没有直接指定这些属性，上述情况也可能发生。例如，为了让 Claude 完成对 cpp-httplib 的 OSS-Fuzz 证明，必须排除因 std::set 析构函数中递归过深而导致堆栈溢出的可能性。递归深度受限于树的最大深度，因此 Claude 不得不在机器代码层面证明，libc++ 的红黑树再平衡算法已正确优化，从而确保树的深度保持在对数级有界。
其他形式化验证案例研究
形式化验证是一个广阔的领域。前文提到的从模糊测试到证明的案例，只是 LLM 通过直接对机器代码应用证明，使形式化验证更易于被广泛采用的一个实例。
我们还发现，利用 LLM 进行形式化验证在其他方式上也取得了成功。例如，我们让 Claude 为 RFC 1950（定义 zlib 压缩文件格式的技术文档）编写一份形式化规范。随后，Claude 证明了 Linux 内核中的 zlib 实现正确实现了该规范。与之前的示例类似，Claude 在二进制层面证明了这一性质，只不过此次不是 RISC-V，而是 Claude 直接对使用 x86 编译的二进制文件进行了证明，其中使用了由 Claude 生成（并经过大量测试）的 x86 ISA 形式化语义。7 之后，我们对另外六个广泛使用的库重复了这一过程。在此期间，我们在一些边缘角落案例中发现了少量（不可利用的） bug，这些 bug 正在上游提交修复的过程中。从这个实践中我们得出两个结论：（1）这些经过极其充分测试的代码库已经几乎完全正确；（2）有可能证明真实现有代码库的端到端正确性属性。
在另一项实验中，我们让 Claude 用 Rust 开发了一个大型 Python 子集的解释器，并证明（使用 Verus，一种 Rust 验证工具）它符合某篇学术论文中概述的 CPython 语义。随后，我们通过实际测量其对 CPython 行为的遵循程度，运行了超过 170 万个随机生成的 Python 程序，结果发现 99.95% 的测试中行为与 CPython 完全一致，而剩余的差异均为令人意外的已知边缘角落案例。
我们还尝试用形式化验证来检验一些简单的安全属性，结果在多个广泛使用的关键应用中发现了问题。其中一例是一个潜伏了十多年、此前从未被发现过的逻辑漏洞。在验证某款广泛使用的 PDF 阅读器时，我们一周内发现的安全漏洞数量，相当于通常一整年的报告量。
关于这些工作的更多细节，参见附录。
这只是开始
LLM 辅助形式化验证的一个关键局限在于，证明过程可能需要消耗数亿 token。如果要让整个软件生态都能用上这些方法，成本效率至关重要。幸运的是，有充分的理由相信效率会不断提升。
新模型消耗的 token 更少
我们基于真实的 OSS-Fuzz 代码构建了 36 个小型验证任务。Opus 5.5 能证明其中一半，且 token 消耗比 Opus 5 少约 40%。随着模型在长程验证任务上不断训练，我们预计这一趋势会持续下去。
证明可以复用
当智能体独立工作时，往往会产生大量重复劳动。证明与软件类似，由更小的证明递归构建而成——证明单元越小，通常越易于复用。为了衡量这一机制的影响，我们在让智能体证明各自目标的同时，允许它们相互拷贝对方的证明。在拥有这个共享工作区的情况下，智能体所需的 Token 数比单独工作时减少了 17%，一些智能体甚至在之前独立尝试失败后，借助共享环境成功完成了任务。
我们在 OSS-Fuzz 证明工作中也观察到了大规模发生的类似现象。大多数证明涉及所有程序都包含的代码（特别是 C 运行时和 AddressSanitizer 的初始化），因此差异极大的程序往往会有大量重叠的证明内容。智能团队利用这一点，通过拷贝其他团队已完成的证明并适配到自身程序中来实现优化（图 6）。
证明的这种可复用性，正是 Lean 形式数学共享库 Mathlib 得以成长的原因：目前它已收录近 30 万条定理，由超过 700 位贡献者提交；每一个新证明都建立在前人工作成果之上。我们在 OSS-Fuzz 项目的推进过程中也积累了类似的证明库，其中部分内容已包含在发布版本中（对于可能暴露开源软件未修补漏洞的证明，我们不予发布）。
在走出这些初步实验阶段后，我们需要制定一套策略，以验证庞大的现有软件存量，从最关键的依赖项入手。如前所述，通过采用通用规格并在二进制层面进行操作，我们无需将整个代码库重写为另一种语言，即可实现大规模验证。
这种方法还促进了证明在包级别粒度的复用，意味着每个依赖项只需验证一次。依赖关系遵循幂律分布：只要证明哪怕一小组共享库，就能让大量软件变得可行且可验证。更多细节，请参阅 Theorem 关于验证整个 Nix 生态系统的路线图，其中包括 glibc、OpenSSL 和 cURL 等关键基础设施。
局限性
在实际应用中，形式化验证有时对代码安全性的证明能力不及我们的期望。
“经过形式化验证”不等于“没有 bug”。Claude 可以写出证明，表明编译后程序的行为满足形式化规格（spec）的要求（该规格由外部证明检查器验证）。但证明检查器无法告诉你规格是否符合现实。要贴合现实，规格必须正确地涵盖并建模被验证程序所运行的真实机器的一切，包括 CPU 和操作系统。已验证代码中之所以还会出现 bug，正是因为规格或假设的机器语义与现实存在偏差。好消息是，这也意味着我们知道该去哪里找剩余的 bug，也知道如何设计系统来把这些仍可能有 bug 的空隙降到最小。下面说明这些情况如何体现在我们的证明中，以及未来可以如何弥补这些空隙。
真实机器的行为超出了模型的描述。我们的证明针对的是链接 musl libc 的单线程静态 RISC-V 二进制文件。但大多数人实际使用的是 x86 或 ARM 上的这些库，并动态链接 glibc。要弥合这个差距，我们需要更贴近实际部署环境的系统模型。比如，第一步可以为 x86 生成准确的语义。
验证的命题可能没覆盖所有我们关心的问题。我们证明了：在 Google OSS-Fuzz 的许多 fuzzing 入口（包括 ASan 崩溃检测）上，任何小于 64 MB 的输入都不会触发崩溃。但 ASan 并不能检测所有内存安全问题，而且我们也没有验证每个库的全部入口点。即便验证了所有入口点，也不等于覆盖了整个库（尤其是存在死代码的情况）。此外，真实程序可能会误用库，导致调用方一侧出现内存损坏。要弥合这个差距，我们需要为每个公开函数明确规定调用方必须满足的条件，并且调用方必须严格遵守。
我们预计，随着我们在利用 LLM 进行形式化方法方面积累更多经验，以及模型持续进步，这些局限将逐步被攻克，我们将能够验证我们所依赖代码中更大的比例。
结语
趋势清晰：形式化验证曾只对那些由专家手工打造的、用于最关键安全代码的定制化保证才具备实用性，但很快，它将达到与今日模糊测试几乎相同的普及程度，可用于几乎所有生产级软件。就像静态类型、测试框架和其他正确性工具一样，验证技术将不再只是“外挂”，而是“内置”，其驱动力不仅来自 LLM，还来自语言设计与开发流程的创新。
在当今这个 LLM 自动扫描并发现越来越多代码漏洞的世界里，我们必须采用能够保证代码安全属性的流程。LLM 驱动的大规模形式化验证，是一种有前景的方法，能在过去无法企及的广度和深度上确保这些安全保证。我们鼓励更多人与之实验，共同构建一个稳健软件广泛普及、软件缺陷清晰且可迅速修复的世界。
脚注
01RISC-V 是一种处理器设计，类似于 x86 或 ARM，它定义了软件编译后的汇编指令（芯片执行的基本命令）。
02 入口点是代码的前门，由作者提供用于测试。任何导致崩溃的入口点输入，都是作者关心的 bug。
03 增加此操作需要简单的人工努力：更改参数并重新生成规范，然后让 Claude 重新证明该陈述。
04AddressSanitizer 是一个编译器工具，它为程序添加检查，使得内存错误（如缓冲区溢出和 use-after-free）在运行时发生的那一刻被检测并报告。
05 从技术上讲，这也意味着我们必须信任 Rocq 证明检查器所依赖的硬件、操作系统以及 OCaml 编译器。
06需要注意的是，这种做法也给“奖励作弊”（reward hacking）留下了空间。奖励作弊指的是 AI 模型找到了一条技术上有悖初衷的捷径——看似达成了给定的目标，实际上却没做该做的事，就像学生靠背答案蒙混过关，而不是真正掌握知识。在这个场景下，Claude 完全可能通过把程序改写成永远不会崩溃的版本，来让任何定理都“可证明”。为了防止这种情况，我们对每一次代码补丁都施加了惩罚，并额外奖励它证明补丁会改动哪些输入、改动有多少。同时，我们还记录并审查了所有补丁，排查这类问题。
07我们认为，Claude 能够完全自主地生成一个 ISA 的形式化语义，这本身是另一个有意思的经验。虽然我们无法保证语义百分之百准确，但实测表明，用我们的语义进行单步执行，可以在 Linux 内核之上启动 Ubuntu 用户空间。生成语义的过程中还发现了官方参考文档中的数百处错误，以及硬件本身的一些 bug。