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现在很容易就能 查找 以及 漏洞利用。针对网络攻击的标准防御手段已不再足够：我们需要能够证明代码无缺陷的方法。形式化软件验证可以提供这种保证，但它历来需要多年的专家努力，使其对大多数现实世界的项目而言并不实用。在一项与 定理然而，我们证明情况已不再如此：LLM 现在能够大规模生成形式化证明，从而催生出包含已证明安全保证的全新软件开发工作流。利用 Claude，我们在超过 100 个真实世界的开源软件库中证明了汇编代码层面（RISC-V）的安全属性。 据我们所知,这是首次大规模尝试使用AI在汇编代码层面对生产软件进行形式化验证。 在撰写证明的过程中，Claude还发现了多年来一直未被察觉的漏洞，尽管 trillions of test runs。随着模型能力的不断提升，我们期望形式化验证成为安全软件开发的重要组成部分。
简介
即使是成熟、经过大量测试的软件也包含错误，而大语言模型更是 日益熟练 在发现漏洞方面。Linux 内核——当今测试最充分的软件之一，部署在全球数十亿台设备上——最近出现了 超过 1,000 个漏洞 披露。随着前沿模型的能力日益增强， 将看似无害的漏洞串联起来 要将其转化为关键的漏洞利用，我们需要能够在这些漏洞被实际利用之前检测并修复它们的技术。
理想情况下，这类技术能够找到并修补 所有漏洞， 然后提供某种证明，表明不再存在其他漏洞。 形式化验证 就是实现这一目标的一种方法。在形式化验证中，开发者将他们的代码转化为一个数学模型，然后尝试证明该代码始终遵循某个已定义的安全规则集合。如果他们无法证明这一点，这意味着代码中可能存在一个会违反某条规则的漏洞，而验证失败的性质则暗示了该漏洞可能是什么。重复这一过程（每次都消除导致失败的原因）最终将得出证明，表明代码中不存在任何会违反这些规则的漏洞。
然而，形式化验证并不容易。证明可能比原始代码大许多倍，撰写证明需要巨大的精力以及一种小众且高度专业化的技能。例如，实现 seL4 操作系统内核花了2个人年，但 20 个人年 来对其进行形式化验证。因此，形式化验证只在真正关键任务的应用中才有实用性，例如 空中客车的航空电子代码.
但大语言模型正让这件事变得容易得多。前沿模型如今可以完全自主地为真实世界的软件生成正确性证明。为了展示这一点,我们让 Claude 为 123 个开源库证明有用的安全属性,包括证明其中一些可执行工件能够 绝不 在某些条件下会崩溃。具体而言，Claude 证明了对于每一个小于 64 MB 的输入，以及每一种被建模的 Linux 操作系统（OS）响应和内存布局，在某些假设下（即该程序作为一个单线程静态二进制文件，在 RISC-V1 使用Linux操作系统的CPU)。这仍然远不能解决 全部 它虽然不能保证找出所有可能的错误，但确实让我们比以前更接近这一目标，并为实现该目标提供了路线图。
我们正在发布这些证明的 一个子集 以便任何人都可以验证并复用它们，同时发布的还有 RISC-V 和 OS 语义. 定理，我们在此项目中的合作者，也愿意为 其他开源项目运行相同的流程，并发布了一个 Claude skill 来帮助开发者入门验证自己的代码。
形式化验证是一个广阔的领域，包含许多方法论。下面，我们还描述了使用其他形式化验证方法来加速其他安全或软件开发任务的初步探索，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器的行为等价性，以及找出关键软件中长期存在的漏洞。
形式化验证的前景是光明的。随着模型变得更加智能，编写证明的成本正在下降。此外，随着越来越多的代码被形式化以及实现安全保证的方法变得更加标准化，跨代码库复用或修改证明的能力将摊薄成本。我们鼓励所有开发者探索将形式化验证与 LLM 结合使用——尤其是 那些以前用能力较弱的模型尝试过并发现行不通的人。
在本文的其余部分，我们将更详细地介绍我们的形式化验证实验。
将测试转化为证明
要证明一个软件是正确的，我们必须首先说明“正确”到底意味着什么。正确性由 规范 （spec）定义。在某些程序中，有一种明确的方式来形式化地指定程序的预期行为。例如，一个 PNG 解码器接收一系列字节，并（按照 RFC 2083）将这些字节解码为相应的图像。但对于大多数程序来说，事情就没那么简单了。对于文本编辑器或网页浏览器来说，“正确”意味着什么？获得全面且无歧义的规范的难度，是大规模验证软件的一大障碍。
为了解决我们试图证明的开源库中代码的这一问题，我们采用的方法是，通过使用一个关于在 Linux 上执行任何 RISC-V 编译的二进制文件意味着什么的通用模型，编码“该测试套件始终通过”这一规则，将其现有的可编译测试套件自动转换为规范。从历史上看，证明这类规范是难以处理的，因为编写一个能够涵盖并论证数万条汇编指令在任何输入下的所有可能行为和交互的证明，本身就极其复杂（而且由此产生的证明往往非常庞大）。这正是当今 LLM 的用武之地：为了一个明确的目标而处理数百万行代码，是 LLM 非常适合的任务。
在这个项目中，我们从 模糊测试开始。在这些测试中，开发者为其代码编写一个接收输入的 入口点2 ，任何导致崩溃的输入都被视为作者关心的漏洞。然后， 模糊测试器， 即一个测试引擎，会在入口点生成大量半随机和变异的输入，以尝试找到漏洞（如图 1 所示）。模糊测试器运行的时间越长，它能发现的漏洞就越多。但这本质上是一个暴力过程，无论你尝试多少输入，都无法保证穷尽每一条可能的代码路径。
为了找出模糊测试本来会暴露的所有 bug，我们把模糊测试转化为一个定义在编译后的 RISC-V 指令之上的规约。该规约指出，模糊测试对于小于 64 MB 的 任何 输入小于 64 MB。3 如果 Claude 能够证明这条规约，那么 RISC-V 上的模糊测试就变得多余了：对该入口点进行模糊测试将永远找不到任何 bug。
我们对 Google 的 OSS-Fuzz 计划中的数百个项目做了这件事，该计划为符合条件的开源项目提供持续的模糊测试。OSS-Fuzz 包含数千个由开发者编写的入口点，这些入口点通过崩溃（例如，在断言失败时）来查找损坏的代码属性。OSS-Fuzz 会自动为 C 和 C++ 程序插桩 AddressSanitizer4 （ASan），使其在内存被不当访问时崩溃（这是软件漏洞的一个 主要成因）。像内存安全这样的广谱规约几乎适用于所有软件。
在几周的时间里， Claude 成功修复了它发现的漏洞，并证明了 123 个不同 OSS-Fuzz 库中的 239 个入口点在任何输入（最大 64 MB）下都不会崩溃。 这些证明作用于编译后的 RISC-V 指令（即可执行二进制文件），包含约 1.8 亿行 Rocq 代码，一个典型的证明长达约 600,000 行，为二进制文件提供安全保证，这些二进制文件的中位长度为 18,000 条 RISC-V 指令。这些证明是通过使用 Theorem 的 RISC-V 指令和 Linux 进程语义将 RISC-V 汇编代码转换为数学模型来构建的。这意味着这些证明目前假设程序作为单线程静态二进制文件运行，具有固定内存预算，并在使用 Linux 操作系统的 RISC-V CPU 上执行。扩大这些证明的范围完全可行，因为它只需为更多汇编架构和其他操作系统进程标准化语义。参见 一位专家的观点 ，了解其对 Claude 所写证明的看法。
虽然这是极其庞大的证明代码量，但几乎不需要任何人工审查。Rocq 证明检查器确保规范被证明正确满足。因此，开发者需要信任的仅有以下内容：
- RISC-V 和 Linux 进程的形式化模型；
- 所证明的精确定理陈述；
- Rocq 证明检查器本身。5
这并不意味着这些库中没有漏洞。 而是意味着任何 剩余的漏洞要么存在于上述所列的组件中，要么超出了 Claude 证明的范围。加固这些仍可能存在漏洞的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但与调试这些规模化证明所覆盖的每一行代码相比，这是一项容易得多的任务——尤其是这种方法可以在不增加可信组件规模的情况下保护任意数量的项目。
我们欢迎对我们证明的独立验证，并鼓励对方法的改进。为此，我们正在发布本项目中尚未公开的可信组件（如上所述）；Claude 为无需修补的模糊测试编写的完整 Rocq 证明；以及我们未能证明的其他模糊测试的规范。
发现并修复漏洞
如上所述，我们展示了可以将许多开源库的开发者编写的测试（模糊测试）转化为 Claude 能够证明始终通过的规范，有时需先修复其发现的剩余漏洞。因此，尝试证明这些规范的过程发现了数百个漏洞。
在 Claude 尝试证明数百个入口点期间，出现了大量漏洞。为确保 Claude 不必在每次遇到漏洞时都停下来等待人工处理，我们允许 Claude 修复它发现的漏洞：它修补代码，这导致规范基于修补后的代码重新生成，然后 Claude 继续证明新的规范。6
我们发现的许多漏洞是模糊测试器几乎不可能找到的。模糊测试器对小的输入进行变异， 通常上限为 1 MB，并且通常依赖代码覆盖率来引导它们发现漏洞。在证明某个库的一个入口点时，Claude 发现其副本中的解压程序存在一个计数器下溢，会导致越界写入，但仅发生在具有某种罕见特定布局的约 20 MB 输入上。其他漏洞还包括：某图像解码器中的越界读取，需要 64 MB 的输入和超过 2 GB 的内存；另一库中的越界读取，需要对同一文件的两个句柄按特定顺序调用；以及在 libexpat 中重新发现的 CVE-2026-56132，其需要深度嵌套的输入。Claude 还发现了根本不会导致崩溃的逻辑漏洞。例如，在证明某个库的内存安全性时，它注意到一个用于限制应用程序可加载哪些文件的功能并不总是被强制执行。
本项目的最终目标是实现一个证明，即经 RISC-V 编译的模糊测试已没有剩余可发现的崩溃。然而，像上述那样的漏洞表明，无论该目标是否达成，这一过程还有另一个好处：仅仅是尝试这一过程就能发现需要修复的真实漏洞。
证明超出内存安全的更多性质
证明一个模糊测试没有更多的崩溃可发现，比听起来更有意义。现实世界代码中的模糊测试通常会测试有意义的高层属性是否被违反，例如编码-解码往返一致性、幂等性、代数定律、差分测试、自洽性或与参考实现的等价性。例如，针对 LZO 压缩算法的模糊测试会断言：如果你压缩一个输入，然后再解压它，结果与原始输入相同。如果该属性不成立，程序就会崩溃——因此证明该测试永远不会崩溃等价于证明该属性本身。
即使这些属性并非由开发者直接指定，这种情况也可能发生。例如，为了让 Claude 完成其对 cpp-httplib 的 OSS-Fuzz 证明，有必要排除 std::set 析构函数中因过多递归导致栈溢出的可能性。这个递归深度受树的最大深度限制，因此 Claude 必须证明（在机器代码上！）libc++ 的红黑树重新平衡算法被正确优化，使树的深度保持对数级上界。
其他形式化验证案例研究
形式化验证是一个广阔的领域。上面的模糊测试转证明的例子是 LLM 通过将证明直接应用于机器代码而使形式化验证更广泛可用的一个实例。
我们还以其他方式看到了将 LLM 与形式化验证结合使用的成功。例如，我们让 Claude 为 RFC 1950——定义 zlib 压缩文件格式的技术文档——编写形式化规范。然后，我们让 Claude 证明 Linux 内核中的 zlib 实现正确地实现了该规范。与上面的例子一样，Claude 是在二进制层面证明这一属性的，但这次不是 RISC-V，Claude 使用其自己生成（并经过大量测试）的 x86 ISA 形式化语义，直接证明了 x86 编译的二进制文件。7 随后，我们对另外半打广泛使用的库重复了这一过程。在此过程中，我们在一些边界情况中发现了一些轻微的（不可利用的）漏洞，目前正在向上游提交。我们从这一练习中得出两个结论：(1) 这些经过极度充分测试的代码库已经几乎完全正确，(2) 对真实现有代码库证明端到端的正确性属性是可能的。
在另一个实验中，我们让 Claude 用 Rust 开发一个覆盖 Python 大部分子集的解释器，并证明（使用 Verus，一个 Rust 验证工具）它符合一篇学术论文中概述的 CPython 语义。然后我们通过运行超过 1.7 百万个随机生成的 Python 程序，实证测量了其与 CPython 行为的一致性，在 99.95% 的测试中发现了与 CPython 完全相同的行为，其余测试差异都是不足为奇的已知边界情况。
我们还通过对简单安全属性的形式化验证尝试，在若干广泛使用且关键的应用中发现了问题。在其中一例中，我们发现了一个潜伏超过十年的此前未知的逻辑漏洞。在验证一个广泛使用的 PDF 阅读器的过程中，我们一周内发现的安全漏洞数量通常相当于一年报告的数量。
参见 附录 以了解其中一些工作的更多细节。
这仅仅是开始
LLM 辅助形式化验证的一个关键局限是，生成证明可能需要数亿个 token。如果我们的目标是让这些方法对整个软件生态系统可用，成本效率至关重要。幸运的是，有充分的理由期待效率会得到改善。
更新的模型需要更少的 token
我们构建了36个小型验证任务 构建了 36 个小型验证任务。Opus 5.5 以比 Opus 5 少约 40% 的 token 证明了其中的一半。我们预期随着模型在长验证任务上接受训练，这一趋势将会持续。
证明可以被复用
当智能体各自独立工作时，它们往往最终会重复大量努力。证明与软件一样，是由更小的证明递归构建的——而证明越小，它们往往越可复用。为了衡量这一点的影响，我们允许智能体在证明各自目标时互相复制证明。在获得这个共享工作区后，智能体比单独工作时少用了 17% 的 token，有些智能体甚至在之前单独尝试失败后获得了成功。
我们在 OSS-Fuzz 证明工作中观察到同样的现象大规模发生。证明的大部分内容涉及每个程序都包含的代码（尤其是 C 运行时和 AddressSanitizer 的初始化），因此截然不同的程序最终可能产生高度重叠的证明。智能体团队利用了这一点，复制其他团队已完成的证明，然后将其适配到自己的程序上（图6）。
这种证明的可复用性正是 Mathlib，这是 Lean 中的一个形式化数学共享库，增长至接近 300,000个定理 由700多位贡献者提交:每个新证明都建立在现有的工作成果之上。在开展OSS-Fuzz工作的过程中,我们也积累了类似的证明集合,其中一部分已包含在此次发布中(我们不发布可能泄露开源软件中未修补漏洞的证明)。
随着我们从这些初步实验中毕业，我们需要一个策略来验证庞大的 现有 软件，从最关键的依赖项开始。正如我们所展示的，这可以通过使用通用规范并在二进制级别操作来大规模实现，从而避免了用另一种语言重写整个代码库的需要。
这种方法还便于在包级粒度上重用证明，这意味着每个依赖项只需验证一次。依赖项呈幂律分布：即使是少量共享库的证明也能使大量软件的证明变得可行。更多详情，请参见 Theorem 的路线图 用于验证 Nix 生态系统的整体，其中包括 glibc、OpenSSL 和 cURL 等关键基础设施。
局限性
在实践中，形式化验证有时能证明的代码安全性比我们期望的要少。
“经形式化验证”并不等于“没有漏洞”。 Claude 可以写出证明，表明编译后程序的行为满足形式化规范的要求（该证明由外部证明检查器验证）。然而，证明检查器无法告诉你规范是否符合现实。要与现实相符，规范必须正确地涵盖并建模已验证程序所运行的真实机器的一切，包括 CPU 和操作系统。当已验证的代码中出现缺陷时，原因在于规范或所假设的机器语义与现实不符。幸运的是，这也意味着我们知道 其中 寻找剩余的漏洞，以及如何设计一个将这些仍然可能存在漏洞的缺口降到最低的系统。以下是这些方法如何应用于我们的证明，以及未来可以弥合这些缺口的工作思路。
真实机器做出了模型没有描述的事情。 我们的证明针对的是与 musl libc 链接的单线程静态 RISC-V 二进制文件。然而，大多数人是在 x86 或 ARM 上运行这些库，并与 glibc 动态链接。要弥合这一差距，我们需要更接近已部署系统的系统模型。例如，为 x86 生成准确的语义将为此迈出一步。
该声明可能无法涵盖我们关心的所有内容。 我们证明了在 Google OSS-Fuzz 的许多模糊测试入口点上，对于任何小于 64 MB 的输入，崩溃都不会触发，包括 ASan 崩溃。然而，ASan 并不能检测所有内存安全漏洞，而且我们没有验证每个库的所有入口点。即使我们验证了，仅验证所有入口点也无法覆盖整个库（尤其是当存在死代码时）。此外，真实程序可能会误用该库，导致其中的内存损坏 来电者. 为了弥合这一差距，我们需要为每个公共函数明确规定调用者必须做什么，而调用者也必须严格遵守。
我们预计，随着我们对如何利用LLM进行形式化方法研究的深入了解，以及模型不断改进，这些局限将变得可以解决，届时我们将能够验证我们所依赖的代码中更大比例的部分。
结论
发展轨迹已经清晰：形式化验证历来只适用于在最高安全关键代码中由专家手工打造的定制化保障，但它很快就会像今天的模糊测试一样，几乎对所有生产软件都切实可行。正如静态类型、测试框架和其他正确性工具一样，验证将从“外挂式”走向“内置式”，这一转变不仅由大语言模型驱动，也得益于语言设计和开发工作流方面的创新。
在当今世界——大语言模型（LLM）会自动扫描并发现越来越多的代码漏洞——我们必须采用能够的流程 保证 代码安全属性。基于LLM扩展的形式化验证是一种很有前景的方法，能够在以前无法企及的范围和规模上保障这些保证。我们鼓励其他人进行实验，以便我们能够共同构建一个世界，在这个世界中，健壮的软件得到非常广泛的普及，而软件缺陷成为一种被充分理解、能够快速处理的罕见情况。
脚注
01RISC-V 是一种处理器设计，如同 x86 或 ARM，它定义了软件所编译成的汇编指令（芯片执行的基本命令）。
02入口点是代码的前门，由其作者提供用于测试。任何导致崩溃的入口点输入都是作者关心的 bug。
03增加这一点只需耗费极少的人力来更改参数并重新生成规范，然后让 Claude 重新证明该命题。
04AddressSanitizer 是一种编译器工具，它为程序添加检查，以便在运行时一发生内存错误（例如缓冲区溢出和释放后使用）就立即检测并报告。
05这在技术上还意味着我们必须信任 Rocq 证明检查器所依赖的硬件、操作系统和 OCaml 编译器。
06注意，这为奖励作弊留下了空间。奖励作弊是指 AI 模型找到一个在技术上达成既定目标、却没有做到实际意图的捷径，就像一个学生靠背答案而不是学习知识来通过考试。在此情境下，Claude 可能通过把程序改写成某个轻易永不崩溃的版本而使任何定理都可被证明。为了阻止这种做法，我们对任何补丁都施加了惩罚，并对证明它改变了哪些输入以及这些输入有多少的证明给予额外加分。我们还记录并审计了补丁是否存在这些失败模式。
07我们认为，Claude 能够——完全自主地——生成一个 ISA 的形式语义，这本身是一个独立而有趣的启示。虽然我们无法确定我们的语义本身是完美的，但从经验上看，我们发现通过我们的语义进行单步执行，可以在 Linux 内核之上启动一个 Ubuntu 用户空间。生成这些语义还在官方参考文档中发现了数百处错误，以及硬件本身中较少数量的 bug。