LLMs are making formal software verification feasible at a much larger scale

大型语言模型正在使形式化软件验证在更大规模上成为可能 \ Anthropic

第一章：引言

大型语言模型正在使形式化软件验证在更大规模上成为可能

• 发布时间：2026年10月22日

• 团队：Frontier Red Team

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

大多数软件都布满漏洞，而人工智能现在可以轻松发现并利用这些漏洞。传统的网络攻击防御手段已不再足够：我们需要能够证明代码无漏洞的方法。形式化软件验证可以提供这种保证，但历史上需要专家耗费数年时间，这使得它对大多数实际项目来说不切实际。然而，通过与Theorem的合作，我们证明情况已不再如此：大型语言模型现在可以大规模生成形式化证明，使包含可验证安全保证的新软件开发流程成为可能。使用Claude，我们在超过100个真实世界开源软件库的汇编代码层面（RISC-V）证明了安全属性。据我们所知，这代表了首次在汇编代码层面使用人工智能对生产软件进行形式化验证的大规模尝试。在编写证明过程中，Claude还发现了那些即使经过数万亿次测试运行也未能被发现的漏洞。随着模型能力的持续提升，我们预计形式化验证将成为安全软件开发不可或缺的组成部分。

引言

即使是经过充分测试的成熟软件也包含漏洞，而大型语言模型在发现这些漏洞方面正变得越来越擅长。Linux内核——当今最经过严格测试的软件之一，部署在全球数十亿台设备上——最近披露了超过1000个漏洞。随着前沿模型越来越擅长将看似无害的漏洞串联成关键性攻击，我们需要能够在这些漏洞被利用之前检测并修复它们的技术。

理想情况下，这些技术可以找到并修补所有漏洞，然后提供某种证明表明没有更多漏洞存在。形式化验证是实现这一目标的一种方式。在形式化验证中，开发人员将代码转换为数学模型，然后尝试证明它始终遵循某些定义的安全规则。如果无法证明这一点，这意味着代码中可能存在违反规则的漏洞，而失败的性质暗示了漏洞可能是什么。重复这一过程（每次消除失败原因后），最终将得出代码中不存在任何违反这些规则的漏洞的证明。

然而，形式化验证并不容易。证明可能比原始代码大许多倍，编写它们需要大量努力和高度专业化的技能。例如，实现seL4操作系统内核耗时两年人力，但对其进行形式化验证却耗时20年人力。因此，形式化验证仅在真正关键任务的应用中（如空客的航空电子设备代码）才具有实际可行性。

但大语言模型（LLMs）正在让这一过程变得前所未有的简单。前沿模型现在可以完全自主地为现实世界的软件生成正确性证明。为了证明这一点，我们要求Claude在123个开源库中验证有用的安全部件，包括证明在某些条件下，部分可执行组件永远不会崩溃。具体而言，Claude证明了这些程序在特定假设下（即程序以单线程静态二进制文件形式运行，使用固定内存预算在RISC-V 1 CPU上运行Linux操作系统），对于所有小于64 MB的输入以及所有建模的Linux操作系统（OS）响应和内存布局，程序将始终正常退出，而不会触发内存安全错误或断言失败。这距离解决所有可能的错误还有很长的路要走，但它确实比以往更接近目标，并为实现这一目标提供了清晰的路线图。

我们正在发布这些证明的一部分，以便任何人都可以验证和复用它们，同时附带RISC-V和操作系统语义。我们在这个项目中的合作伙伴Theorem也表示，愿意为其他开源项目运行相同的验证流程，并发布了Claude技能，帮助开发者开始验证自己的代码。

形式化验证是一个涵盖众多方法的广泛领域。下面，我们还描述了我们使用其他形式化验证方法进行的初步探索，以加速其他安全或软件开发任务，例如评估zlib压缩算法的安全性、证明用Rust编写的Python解释器的行为等价性，以及根除关键软件中的长期存在的错误。

形式化验证的未来充满希望。随着模型变得越来越智能，编写证明的成本正在下降。此外，随着更多代码被形式化，以及实现安全保证的方法变得更加标准化，跨代码库复用或修改证明的能力将分摊成本。我们鼓励所有开发者尝试使用大语言模型进行形式化验证——特别是那些之前尝试过但使用能力较弱的模型并发现效果不佳的开发者。

在本文的其余部分，我们将更详细地介绍我们的形式化验证实验。

将测试转化为证明

要证明某个软件是正确的，我们首先必须明确“正确”到底意味着什么。正确性由规范（spec）定义。在某些程序中，存在明确的方式可以形式化地指定程序的预期行为。例如，PNG解码器接收字节序列，并按照RFC 2083标准将这些字节解码为对应的图像。但对大多数程序而言，情况并不这么直接。一个文本编辑器或网页浏览器的“正确”意味着什么？获得全面且无歧义的规范的难度，是大规模验证软件的重大障碍。

为了解决我们试图证明的开源库中代码的问题，我们采用自动将它们现有的可编译测试套件转换为规范的方法，通过编码规则“该测试套件始终通过”，并使用一个通用模型来描述在Linux上执行任何RISC-V编译二进制文件的含义。历史上，证明此类规范一直具有挑战性，因为编写能够涵盖并论证数以万计汇编指令在任意输入下所有可能行为和交互的证明本身具有内在复杂性（且证明规模通常会变得极其庞大）。这就是当前大语言模型（LLMs）发挥作用的地方：处理数百万行代码以实现明确目标的任务，LLMs非常擅长。

对于该项目，我们从模糊测试（fuzz tests）入手。在这些测试中，开发人员会编写一个入口点，该入口点接收输入，任何导致崩溃的输入都是作者关注的漏洞。然后，模糊测试引擎会生成大量半随机和变异的输入，通过入口点尝试发现漏洞（如图1所示）。模糊测试运行时间越长，发现的漏洞越多。但本质上这是一个暴力搜索过程，无论尝试多少输入，都无法保证覆盖所有可能的代码路径。

模糊测试通过将大量生成的输入传递给一个入口点，寻找导致崩溃的输入。由于输入是无限的，搜索永远无法完成。

为了找出模糊测试可能揭示的所有漏洞，我们将模糊测试转换为基于RISC-V指令的规范。该规范声明：对于任何小于64 MB的输入，模糊测试不会崩溃。如果Claude能够证明该规范，那么在RISC-V上的模糊测试就变得多余了：对这个入口点进行模糊测试将永远无法发现任何漏洞。

我们在Google的OSS-Fuzz计划中对数百个项目执行了此操作，该计划为符合条件的开源项目提供持续的模糊测试。OSS-Fuzz包含数千个由开发人员编写的入口点，这些入口点通过崩溃（例如在断言失败时）来寻找代码缺陷。OSS-Fuzz会自动使用AddressSanitizer（ASan）对C和C++程序进行插桩，使其在内存访问不当时立即崩溃（这是软件漏洞的主要原因之一）。像内存安全性这样的广谱规范几乎适用于所有软件。

开源库及其现有的模糊测试被编译为RISC-V可执行文件。该可执行文件，加上Theorem的RISC-V和操作系统形式语义，以及期望的无崩溃属性，机械地生成证明必须满足的规范。Claude编写证明；Rocq内核将其与规范进行验证。绿色标记表示已证明的内容，前提是受信任组件正确无误。

在数周时间内，Claude 成功修复了其发现的漏洞，并证明了在 64 MB 输入限制下，123 个不同 OSS-Fuzz 库中的 239 个入口点均不会发生崩溃。这些证明基于编译后的 RISC-V 指令（即可执行二进制文件），总共包含约 1.8 亿行 Rocq 代码，单个证明通常需要约 60 万行代码，以确保对包含 1.8 万条 RISC-V 指令的二进制文件提供安全保证。这些证明通过将 RISC-V 汇编代码转换为数学模型实现，模型基于 Theorem 的 RISC-V 指令集和 Linux 进程语义。这意味着当前证明假设程序在 RISC-V CPU 上以单线程静态二进制形式运行，且内存预算固定，操作系统为 Linux。扩展这些证明的范围完全可行，只需要为更多汇编架构和其他操作系统进程标准化语义。可参见专家对 Claude 编写的证明的分析。

针对所有输入的正式无崩溃证明可以排除从入口点可达路径上的所有崩溃情况。在迭代证明过程中，Claude 还能发现并修复所有剩余的可达崩溃漏洞。

尽管证明代码量巨大，但几乎无需人工审查。Rocq 证明检查器确保证明满足规范要求。因此，开发者只需信任以下内容：

• RISC-V 和 Linux 进程的正式模型；
• 已证明的精确定理陈述；
• Rocq 证明检查器本身。

这并不意味着这些库中没有漏洞。实际上，这意味着剩余的漏洞要么存在于上述列出的组件中，要么超出 Claude 证明的范围。强化这些仍可能存在漏洞的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但与调试扩展证明所覆盖的每一行代码相比，这是一项更可行的任务——特别是这种方案可以在不增加可信组件规模的情况下，为任意数量的项目提供安全保障。

我们欢迎对证明的独立验证，并鼓励对方法进行改进。为此，我们将发布本项目中尚未公开的可信组件（如上所述）、Claude 为无需补丁的模糊测试编写的完整 Rocq 证明，以及其他我们未能证明的模糊测试的规范。

发现并修复漏洞

如上所述，你可以将许多开源库的开发者编写的测试（模糊测试）转换为 Claude 可证明始终通过的规范，有时需要先修复 Claude 发现的剩余漏洞。因此，尝试证明这些规范的过程发现了数百个漏洞。

在 Claude 尝试证明数百个入口点的过程中，出现了大量漏洞。为确保 Claude 不需要每次遇到这种情况都暂停等待人工干预，我们允许 Claude 修复其发现的漏洞：它会修补代码，使规范基于修补后的代码重新生成，然后 Claude 继续证明新的规范。

我们发现的许多漏洞是模糊测试工具几乎不可能发现的。模糊测试工具通常对小输入进行变异（通常限制在1 MB以内），并依赖代码覆盖率来引导其发现漏洞。在证明某个库的入口点时，Claude发现其解压器副本中的计数器下溢漏洞，导致越界写入，但该漏洞仅在约20 MB且具有特定罕见布局的输入下才会触发。其他漏洞包括一个需要64 MB输入和超过2 GB内存的图像解码器越界读取漏洞，另一个库需要对同一文件的两个句柄执行特定调用序列才能触发的越界读取漏洞，以及在libexpat中重新发现需要深度嵌套输入的CVE-2026-56132漏洞。Claude还发现了永远不会导致崩溃的逻辑错误。例如，在证明某个库的内存安全性时，它发现了一个用于限制应用程序可加载文件范围的功能并未始终强制执行。

该项目的最终目标是证明RISC-V编译的模糊测试用例已没有剩余可发现的崩溃。然而，上述漏洞表明，无论是否实现该目标，这一过程本身就有其他价值：即使只是尝试这一过程，也能发现需要修复的真实漏洞。

证明的不仅是内存安全性

证明模糊测试用例没有更多崩溃可发现，其意义比表面听起来更大。在现实世界的代码中，模糊测试通常用于检测违反重要高层属性的情况，例如编码-解码往返一致性、幂等性、代数定律、差异测试、自洽性或与参考实现的等价性。例如，LZO压缩算法的模糊测试用例会断言：如果对输入进行压缩后再解压，结果应与原始输入相同。如果该属性不成立，程序就会崩溃——因此证明测试用例永不崩溃等价于证明该属性本身成立。

即使属性未被开发者明确指定，这种情况也可能发生。例如，为了完成cpp-httplib的OSS-Fuzz证明，Claude必须排除因std::set析构函数中递归过深导致栈溢出的可能性。该递归深度受树的最大深度限制，因此Claude必须证明（在机器码层面！）libc++的红黑树再平衡算法已正确优化，以保持树的深度对数级限制。

其他形式化验证案例研究

形式化验证是一个广泛的研究领域。上述将模糊测试转换为证明的案例只是LLMs通过直接将证明应用于机器码，使形式化验证更广泛可用的众多实例之一。

我们还通过其他方式将大语言模型（LLMs）与形式化验证结合，取得了成功。例如，我们要求Claude为RFC 1950编写形式化规范，该技术文档定义了zlib压缩文件格式。随后，我们让Claude证明Linux内核中的zlib实现是否符合该规范。与上述示例类似，Claude在二进制层面证明了这一属性，但这次不是针对RISC-V，而是直接通过Claude生成的（并经过大量测试的）x86指令集架构（ISA）形式化语义，验证了x86编译的二进制文件。我们随后对另外六个广泛使用的库重复了这一过程。在此过程中，我们发现了一些边缘情况中的轻微（不可利用的）漏洞，这些漏洞正在被提交到上游仓库。从这次实践中，我们得出两个结论：（1）这些经过极其严格测试的代码库已经几乎完全正确，（2）可以对真实存在的代码库证明端到端的正确性属性。

在另一项实验中，我们要求Claude用Rust开发一个涵盖Python大部分功能的解释器，并使用Verus（一个Rust验证工具）证明其符合学术论文中描述的CPython语义。随后，我们通过运行超过170万个随机生成的Python程序，对CPython行为进行实证测量，发现99.95%的测试中与CPython的行为完全一致，其余测试差异均为已知的边缘情况。

我们还通过验证简单的安全属性，在多个广泛使用且关键的应用程序中发现了问题。其中一项发现了一个此前未知的逻辑漏洞，该漏洞已潜伏十多年。在验证一个广泛使用的PDF阅读器时，我们在一周内发现了与通常一年报告数量相当的安全漏洞。

有关这些工作的更多细节，请参见附录。

这仅仅是开始

LLM辅助形式化验证的一个关键限制是，证明过程可能需要消耗数亿个token。如果我们的目标是让这些方法惠及整个软件生态系统，成本效率至关重要。幸运的是，有充分的理由相信效率将得到显著提升。

新模型需要更少的token

我们从真实OSS-Fuzz代码中构建了36个小型验证任务。Opus 5.5在验证这些任务时，使用的token数量比Opus 5减少了约40%。随着模型在长验证任务上进行训练，我们预计这一趋势将持续。

Opus 5.5的证明速度比早期模型更快。在给定token预算下，单个代理完成36个形式化验证任务的占比。每个任务在5M-token预算下获得三次独立的单代理尝试，当首次尝试完成时即视为证明成功。

证明可以复用

当代理单独工作时，常常会重复大量工作。证明与软件一样，是通过更小的证明递归构建的——证明越小，复用性通常越高。为了衡量这一影响，我们让代理在证明各自目标时互相复制彼此的证明。当获得这个共享工作区的访问权限时，代理使用的token比单独工作时减少了17%，甚至有些代理在之前单独尝试失败后仍成功完成了证明。

The 36 proofs from one shared workspace, in the order they finished. An arc joins any two proofs that share an unchanged file; bars show the tokens spent writing each proof, and black lines show the same task’s average cost for an agent working alone, which was higher in 30 of the 34 completed proofs (agents working alone were not able to complete two of the proofs).

We observed the same phenomenon occurring at scale during our OSS-Fuzz proof effort. Most of a proof concerns code that every program contains (particularly initialization of the C runtime and AddressSanitizer), so very different programs can end up with significantly overlapping proofs. Agent teams took advantage of this by copying another team’s finished proof and then adapting it to their own program (Figure 6).

Agents copied an existing proof and adapted it to each new program. Each column represents one program’s complete proof by share of bytes. Blocks are the parts of the proof and each block shows how much was kept identical, lightly edited (same file, size within 2%), edited more, or newly written. The shared parts gained almost no new code.

This reusability of proofs is how Mathlib , a shared library of formal mathematics in Lean, grew to nearly 300,000 theorems submitted by over 700 contributors: each new proof builds on the existing body of work. We accumulated a similar body of proofs in the course of our OSS-Fuzz effort, some of which we’re including in our release (we are not releasing proofs that may reveal an unpatched bug in the open-source software).

As we graduate from these initial experiments, we need a strategy for verifying the enormous body of existing software, starting with the most critical dependencies. As we’ve shown, this can be achieved at scale by using generic specs and working at the binary level, sidestepping the need to rewrite entire codebases in another language.

This approach also facilitates the reuse of proofs at package-level granularity, which means that each dependency only needs to be verified once. Dependencies follow a power law: proving even a small set of shared libraries makes a huge swath of software feasible to prove. For more details, see Theorem’s roadmap for verifying the entirety of the Nix ecosystem, which includes critical infrastructure like glibc, OpenSSL, and cURL.

Limitations

In practice, formal verification can sometimes prove less about the security of the code than we would like.

“Formally verified” does not mean “bug-free.” Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality. To match reality, the spec must correctly encompass and model everything about the real-world machine that the verified program runs on, including the CPU and operating system. When bugs show up in verified code, it’s because the spec, or the assumed semantics of the machine, differs from reality. Fortunately, this also means we know where to look for remaining bugs, and how to design a system where those still-possibly-buggy gaps are minimized. Below are the ways this applies to our proofs, and ideas for future work that would close those gaps.

真实机器执行的操作与模型描述的不一致。我们的证明仅针对单线程、静态链接的RISC-V二进制文件，并使用musl libc库。然而，大多数人会在x86或ARM架构上运行这些库，并动态链接到glibc。要弥补这一差距，我们需要更接近实际部署系统的系统模型。例如，迈向这一目标的一步是为x86生成精确的语义。

该声明可能无法涵盖我们所有关注的方面。我们证明了在Google OSS-Fuzz的许多模糊测试入口点（包括ASan崩溃）中，任何64MB以下的输入都不会触发崩溃。然而，ASan无法检测所有内存安全漏洞，我们也没有验证每个库的所有入口点。即使我们做到了这一点，验证所有入口点也无法覆盖整个库（尤其是存在死代码时）。此外，真实程序可能错误使用库，导致调用方发生内存损坏。要弥补这一差距，我们需要为每个公共函数明确调用方必须执行的操作，调用方必须严格遵守这些规定。

随着我们对如何利用大语言模型进行形式化方法的理解加深，以及模型持续改进，这些限制将变得可处理，届时我们将能够验证我们依赖的代码中更大比例的部分。

结论

趋势已经明确：形式化验证过去仅在最安全关键的代码中用于专家定制的保证，如今将很快像模糊测试一样成为几乎所有生产软件的实用工具。就像静态类型、测试框架和其他正确性工具一样，验证将从“附加组件”成熟为“内置特性”，这不仅由大语言模型推动，还由语言设计和开发流程的创新共同驱动。

在当今这个大语言模型能够自动扫描并发现越来越多代码漏洞的世界里，我们必须采用能够保证代码安全属性的流程。基于大语言模型扩展的形式化验证是一种有前景的方法，它能够在前所未有的规模和范围内确保这些保证。我们鼓励其他人进行实验，让我们共同构建一个软件缺陷成为广为人知且能快速解决的罕见现象，而稳健软件广泛普及的世界。

阅读完整附录。

脚注

01 RISC-V是一种处理器设计，类似于x86或ARM，它定义了软件编译成的汇编指令（芯片执行的基本命令）。

02 入口点是代码的入口，由作者提供用于测试。任何导致崩溃的入口点输入都是作者关注的漏洞。

03 增加这一参数需要人类进行微小的修改，重新生成规范，然后让Claude重新证明该声明。

04 AddressSanitizer是一种编译器工具，它向程序中添加检查，以便在运行时立即检测并报告内存错误，如缓冲区溢出和使用已释放内存。

05 从技术上讲，这也意味着我们必须信任Rocq证明检查器所依赖的硬件、操作系统和OCaml编译器。

06 请注意，这为奖励黑客打开了大门。奖励黑客是指AI模型找到一种捷径，虽然在技术上符合其被赋予的目标，但并未真正完成预期的任务，就像学生通过记忆答案而不是学习材料通过考试一样。在此背景下，Claude可以通过将程序重写为永远不会崩溃的简单版本，使任何定理都变得可证明。为了防止这种情况，我们对任何补丁都进行了惩罚，并为证明补丁所修改的输入及其数量的稀少性提供了额外加分。我们还记录并审计了这些补丁，以防范此类失败模式。

07 我们认为，Claude能够完全自主地生成ISA的形式语义是一个值得关注的独立案例。虽然我们无法确定我们的语义本身是否完美，但经验表明，通过单步执行我们的语义，可以在Linux内核之上启动Ubuntu用户空间。生成这些语义还发现了官方参考文档中的数百处错误，以及硬件本身中数量较少的缺陷。