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

本文为原文前 6,000 字符的节选翻译，完整内容请查看原文。

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

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

Most software is riddled with bugs, which AI can now easily find and exploit. The standard defenses against cyberattacks are no longer sufficient: we need ways to prove that code is free of bugs. Formal software verification could provide this guarantee, but it has historically required years of expert effort, making it impractical for most real-world projects. In a collaboration with Theorem, however, we show this is no longer the case: LLMs can now produce formal proofs at large scale, enabling new software development workflows that include proven security guarantees. Using Claude, we proved security properties at the assembly code level (RISC-V) in over 100 real-world open-source software libraries. To our knowledge, this represents the first large-scale effort to use AI to apply formal verification to production software at the assembly code level. While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs. As model capabilities continue to improve, we expect formal verification to become an essential part of secure software development.

大多数软件都充斥着漏洞，而人工智能现在可以轻易地发现并利用这些漏洞。针对网络攻击的标准防御手段已不再足够：我们需要能够证明代码不存在漏洞的方法。形式化软件验证可以提供这种保证，但从历史上看，这需要专家耗费数年时间，使得它对于大多数现实世界的项目来说并不切实际。然而，通过与 Theorem 的合作，我们证明情况已不再如此：大语言模型（LLM）现在可以大规模生成形式化证明，从而实现包含已验证安全保证的全新软件开发工作流。我们利用 Claude 在 100 多个现实世界的开源软件库中证明了汇编代码级别（RISC-V）的安全属性。据我们所知，这是首次大规模利用人工智能将形式化验证应用于生产环境软件的汇编代码级别。在编写证明的过程中，Claude 还发现了那些尽管经过数万亿次测试运行、却多年未被察觉的漏洞。随着模型能力的持续提升，我们预计形式化验证将成为安全软件开发中不可或缺的一部分。

Even mature, heavily tested software contains bugs, and LLMs are increasingly adept at finding them. The Linux kernel—one of the most well-tested pieces of software today, deployed on billions of devices worldwide—recently had over 1,000 vulnerabilities disclosed. With frontier models becoming more capable of chaining seemingly benign bugs into critical exploits, we need techniques that can detect and fix these bugs before they can be exploited in the wild.

即使是成熟且经过严格测试的软件也包含漏洞，而 LLM 在发现这些漏洞方面正变得越来越得心应手。Linux 内核是当今测试最充分的软件之一，部署在全球数十亿台设备上，但最近仍披露了 1,000 多个漏洞。随着前沿模型在将看似良性的漏洞串联成关键攻击方面的能力不断增强，我们需要能够在这些漏洞被野外利用之前就检测并修复它们的技术。

Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found. Formal verification is one way to do this. In formal verification, developers translate their code into a mathematical model, then try to prove that it always follows some defined set of security rules. If they fail to prove this, that means there could be a bug in the code that would violate a rule, and the nature of the failure implies what the bug might be. Repeating this process (after eliminating the cause of failure each time) will ultimately yield proof that the code is devoid of any bug that would violate those rules.

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

However, formal verification isn’t easy. Proofs can be many times larger than the original code, and writing them requires significant effort and a niche, highly specialized skill set. For instance, it took two person-years to implement the seL4 operating system kernel, but 20 person-years to formally verify it. Accordingly, formal verification has been practical only in truly mission-critical applications, such as Airbus’s avionics code.

然而，形式化验证并不容易。证明的规模可能比原始代码大许多倍，编写它们需要巨大的努力以及小众且高度专业化的技能。例如，实现 seL4 操作系统内核耗费了 2 人年，但对其进行形式化验证却耗费了 20 人年。因此，形式化验证仅在真正关键的任务应用中才具有实用性，例如空中客车的航空电子代码。

But LLMs are making it far easier. Frontier models can now produce correctness proofs for real-world software fully autonomously. To demonstrate this, we asked Claude to prove useful security properties across 123 open-source libraries, including showing that some of their executable artifacts can never crash under certain conditions. Specifically, Claude proved that these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB and every modeled Linux operating system (OS) response and memory layout, under certain assumptions (namely that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V1 CPU using Linux OS). This is still far away from fixing all possible bugs, but it does get us much closer than before and provides a roadmap toward that end.

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

We’re publishing a subset of these proofs so that anyone can verify and reuse them, along with the RISC-V and OS semantics. Theorem, our collaborator on this project, is also offering to run the same pipeline for other open-source projects, and is publishing a Claude skill to help developers get started with verifying their own code.

我们正在发布这些证明的一个子集，以便任何人都可以验证和重用它们，以及 RISC-V 和操作系统的语义。我们在此项目中的合作伙伴 Theorem 也提议为其他开源项目运行相同的流水线，并正在发布一项 Claude 技能，以帮助开发人员开始验证他们自己的代码。

Formal verification is a broad field with many methodologies. Below, we also describe our initial explorations using other formal verification methods to accelerate other security or software development tasks, such as assessing the security of the zlib compression algorithm, proving behavioral equivalence of a Python interpreter written in Rust, and rooting out long-standing bugs in critical software.

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

The road ahead for formal verification is promising. The cost of writing proofs is falling as models become more intelligent. Moreover, as more code is formalized and methods of achieving security guarantees become more standardized, the ability to reuse or modify proofs across codebases will amortize the cost. We encourage all developers to explore formal verification with LLMs—especially those who previously tried it with less capable models and found it didn’t work.

形式化验证的前景是光明的。随着模型变得越来越智能，编写证明的成本正在下降。此外，随着更多的代码被形式化，以及实现安全保证的方法变得更加标准化，跨代码库重用或修改证明的能力将分摊成本。我们鼓励所有开发人员探索使用 LLM 进行形式化验证——特别是那些之前尝试过使用能力较弱的模型但发现行不通的开发人员。

In the rest of this post, we cover our formal verification experiments in more detail.

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

To prove that a piece of software is correct, we must first state what “correct” even means. Correctness is defined by the specification (spec). In some programs, there is a clear way to formally specify the program’s intended behavior. For example, a PNG decoder takes a sequence of bytes and (following RFC 2083) decodes these bytes into the corresponding image. But for most programs, things aren’t so straightforward. What would it mean for a text editor or a web browser to be “correct”? The difficulty of obtaining a comprehensive and unambiguous spec is a significant obstacle to verifying software at a larger scale.

为了证明一段软件是正确的，我们必须首先说明“正确”到底意味着什么。正确性由规范（spec）定义。在某些程序中，有一种明确的方法可以形式化地指定程序的预期行为。例如，PNG 解码器接收字节序列，并（遵循 RFC 2083）将这些字节解码为相应的图像。但对于大多数程序来说，事情并没有那么简单。对于文本编辑器或网络浏览器来说，“正确”意味着什么？获取全面且无歧义的规范的难度是更大规模验证软件的一个重大障碍。

To address this for the code in the open-source libraries that we sought to prove, we take the approach of automatically converting their preexisting compilable test suites into a spec by encoding the rule “this test suite always passes,” using a general model of what it means to exec

为了解决我们试图证明的开源库代码中的这个问题，我们采用了一种方法，即通过编码“此测试套件始终通过”这一规则，利用关于执行含义的通用模型，自动将它们预先存在的可编译测试套件转换为规范。