基恩·卢卡斯，安格斯·林奇，卢纳·通，卢克·香，齐吉·斯特拉兹尼卡斯，迪诺·迪斯特法诺，哈希卡·阿格拉瓦尔埃维亚塔尔·本·阿舍尔，阿瓦·豪威尔，萨米·贾瓦尔，克里斯·罗尔夫，尼科莱·泽尔多维奇尼古拉斯·卡尔尼，拉贾斯里·阿格拉瓦尔，杰森·格罗斯
当前软件普遍存在漏洞，且人工智能在挖掘和利用这些漏洞方面的能力日益增强。正式的软件验证虽能提供代码无漏洞的数学证明，但传统上因耗时数年、依赖专家而难以大规模应用。然而，一项与 Theorem 公司合作的研究表明，这一局面正在改变：大语言模型（LLM）已具备大规模生成正式证明的能力。研究团队利用 Claude 模型，对超过 100 个现实世界的开源软件库进行了 RISC-V 汇编层面的安全性验证。据称，这是首次使用 AI 在生产软件的汇编层面进行如此规模的正式验证。即便经过数万亿次测试，Claude 仍发现了多年未被察觉的错误。随着模型能力的提升，正式验证有望成为安全软件开发流程中的核心环节。
背景与挑战
即使是经过严格测试的成熟软件也难免存在缺陷。以 Linux 内核为例，作为全球部署最广泛的软件之一，近期披露的漏洞已超过 1,000 个。随着前沿模型能够更有效地将微小漏洞串联成关键攻击链，业界急需一种能抢先发现并修复漏洞的技术。
正式验证通过构建代码的数学模型来证明其始终符合特定的安全规则。若无法证明，则意味着可能存在违规错误。通过迭代消除故障原因，最终可证明代码不存在违反规则的可能。然而，正式验证门槛极高，编写规范往往比原始代码复杂得多。例如，实施 seL4 操作系统内核仅需 2 个工作年，但其正式验证却耗费了 20 个工作年。因此，过去这种技术仅用于空客航空电子码等极度关键的任务。
LLM 的出现降低了这一门槛。边界模型现在可以自主为真实世界软件提供正确性证明。为了验证这一能力，研究团队要求 Claude 证明 123 个开源库的安全特性。具体而言，Claude 证明了这些程序在特定假设下（即在配备 RISC-V CPU 的 Linux 系统上以单线程静态二进制运行），对于任何小于 64 MB 的输入以及所有模拟的 OS 响应和内存布局，均能正常退出且不引发内存安全错误或断言失败。
目前，部分证明及 RISC-V 和 OS 语义已公开发布，供社区验证和复用。合作伙伴 Theorem 也在为其他开源项目提供类似管道，并发布了一项 Claude 技能，协助开发者启动自身代码的验证工作。此外，团队还探索了其他正式验证方法，如评估 zlib 压缩算法的安全性、证明 Rust 编写的 Python 解释器的行为等价性等。
从模糊测试到形式化证明
证明软件正确性的前提是明确定义“正确”。对于 PNG 解码器等有明确规范（如 RFC 2083）的程序，这相对容易；但对于文本编辑器或浏览器等项目，获取全面明确的规范是大规模验证的主要障碍。
为解决这一问题，团队采用了一种自动化方法：将现有的可编译测试套件转化为规范，编码规则为“该测试套件必须始终通过”，并结合 Linux 上执行 RISC-V 二进制文件的一般模型。历史上，证明此类规范的复杂性在于需涵盖成千上万条汇编指令在所有可能输入下的行为，导致证明体量巨大。这正是 LLM 的优势所在：在追求明确目标时，编写数百万行代码非常适合由 LLM 完成。
项目始于模糊测试（Fuzzing）。开发人员编写接收输入的入口点，任何导致崩溃的输入均被视为 bug。测试引擎随后生成大量半随机和突变输入以寻找错误。虽然长时间运行能发现更多 bug，但这本质上是一个暴力过程，无法保证覆盖所有代码路径。
为了找出所有潜在错误，团队将模糊测试转化为基于编译后 RISC-V 指令定义的规范。如果 Claude 能证明对于任何小于 64 MB 的输入都不会发生崩溃，那么对该入口点的模糊测试就变得多余，因为理论上已排除了所有可达的崩溃路径。
团队在 Google 的 OSS-Fuzz 计划中针对数百个项目实施了这一方法。OSS-Fuzz 包含数千个经授权的入口点，并通过 AddressSanitizer (ASan) 自动检测 C/C++ 程序中的内存访问错误。几乎所有软件都适用“内存安全性”这一广泛规范。
在短短几周内，Claude 成功修复了其发现的漏洞，并证明了在 123 个不同的 OSS-Fuzz 库中的 239 个入口点上，对于任何最大至 64 MB 的输入均不会发生崩溃。这些证明针对编译后的 RISC-V 指令，涉及约 1.8 亿行 Rocq 代码；典型的单个证明约有 60 万行，可为中位长度为 18,000 条 RISC-V 指令的二进制文件提供安全保证。证明通过将 RISC-V 汇编代码转换为数学模型构建，利用了 Theorem 公司的 RISC-V 指令语义和 Linux 进程语义。这意味着目前的证明假设程序以单线程静态二进制形式运行。扩大适用范围完全可行，只需为更多架构和操作系统标准化语义即可。
尽管产生了海量验证代码，但几乎无需人工检查。Rocq 证明检查器确保证明正确满足规格。开发者唯一需要信任的组件包括：RISC-V 和 Linux 进程的正式模型、被证明的确切定理命题、以及 Rocq 检验器本身。这并不意味着库中没有错误，而是剩余错误要么存在于上述可信组件中，要么在 Claude 证明的范围之外。固化这些可信组件比调试每一行代码更容易处理，且该方法可在不增加可信组件大小的情况下确保任意数量的项目。
漏洞的发现与修复
在尝试证明规范的过程中，Claude 发现了数百个错误。为了确保流程自动化，Claude 还被授权修复其发现的代码漏洞。
许多发现的漏洞极难通过传统手段捕捉。模糊器通常限制输入大小在 1MB 以内并依赖代码覆盖率引导搜索。而在某库的解压功能中，Claude 发现了一个计数器下溢导致的越界写入错误，该错误仅在罕见的特定布局的 20MB 左右输入上触发。其他漏洞包括：图像解码器中需要 64MB 输入和 2GB 以上内存才能触发的越界读取；另一库中需要在双处理器环境下对同一文件进行特定调用序列才能触发的越界读取；以及在 libexpat 中重新发现的 CVE-2026-56132，需深度嵌套输入才能触发。Claude 还发现了从未导致崩溃的逻辑错误，例如某库中限制应用程序加载文件的功能并未总是被强制执行。
即使未能完全实现“无剩余崩溃”的目标，这一过程本身也能产生需修复的真实错误，具有显著价值。
超越内存安全的证明
证明“无崩溃”比听起来更重要。现实世界中的模糊测试常检测高层属性违规，如编解码往返一致性、幂等性、代数定律或与参考实现的等价性。例如，LZO 压缩算法的模糊测试断言压缩再解压应与原始输入相同。若属性不成立，程序会崩溃，因此证明测试永不崩溃等同于证明该属性成立。
即使开发者未直接指定属性，情况亦然。例如，为了完成 cpp-httplib 的 OSS-Fuzz 验证，需排除由于 std::set 析构器中递归过深导致堆溢出的可能性。Claude 必须在机器代码层面证明 libc++ 的红黑树再平衡算法正确优化以保持树的深度在对数边界内。
其他案例研究
除了直接将证明应用于机器代码，团队还探索了其他形式的验证：
- zlib 压缩算法：Claude 编写了 RFC 1950 的正式规范，并证明了 Linux 内核中的 zlib 实现在 x86 编译二进制级别正确实现了该规范。过程中发现了角落案例中的微小不可利用错误。结论显示充分测试的代码库已接近完全正确，且端到端正确性属性是可证明的。
- Python 解释器：Claude 开发了一个 Rust 编写的 Python 子集解释器，并使用 Verus 工具证明其符合学术论文中概述的 CPython 语义。实证测量显示，在运行超过 17 万个随机生成的 Python 程序中，99.95% 的情况下其行为与 CPython 一致，差异均为已知角落案例。
- 长期潜伏 Bug：通过对广泛使用的关键应用进行简单安全属性的正式验证，团队在一周内发现的安全漏洞数量相当于一年内报告的总量，其中包括一个潜伏十多年的未知逻辑错误。
成本效益与规模化前景
LLM 辅助形式验证的一个关键局限是证明生成需要消耗数以亿计的 token。若要在整个软件生态系统中推广，成本效益至关重要。但有理由预期效率将持续提升。
新型号降低 Token 消耗
基于真实的 OSS-Fuzz 代码构建的 36 个小验证任务显示，Opus 5.5 相比 Opus 5 减少了 40% 的 token 消耗。随着模型在长时间验证任务上的训练深入，这一趋势预计将继续。
证明的可复用性
当代理独立工作时，往往会重复大量劳动。证明像软件一样是从较小证明递归构建的，较小的证明更易复用。实验显示，允许代理在共享工作空间中互相复制证明时，所需 token 比单独工作时少 17%，部分代理甚至在单独尝试失败后通过协作成功。
在 OSS-Fuzz 项目中，大多数证明涉及程序包含的共同代码（如 C 运行时和 ASan 初始化），导致不同程序的证明存在显著重叠。代理团队利用这一点，复制现有证明并调整以适应新程序。这种可复用性类似于 Mathlib 积累近 300,000 个定理的模式。团队建议优先验证最关键的依赖项，利用包级细分化复用证明，使得每个依赖性只需一次验证即可覆盖大量上层软件。
局限性分析
实践中，正式验证有时不如预期那样完美保障代码安全性。“正式验证”不等于“无错误”。Claude 编写的证明表明编译程序的行为满足外部验证检查器认可的规范，但验证器无法确认规范是否与现实完全匹配。若出现错误，通常是因为规范或机器假设语义与现实不符。
主要差距包括：
- 硬件与系统模型差异：目前的证明针对单线程、静态链接 musl libc 的 RISC-V 二进制。而现实中多数用户运行的是动态链接 glibc 的 x86 或 ARM 架构。弥补这一差距需要为 x86 等架构生成更精确的系统模型。
- 规范覆盖范围：虽然证明了 OSS-Fuzz 入口点在特定输入下不崩溃，但 ASan 并非检测到所有内存安全问题，且并非所有入口点都被验证。此外，调用者滥用库可能导致内存损坏，这需要明确每个公共函数的调用约束。
随着模型改进，这些局限性将变得更具可操作性，从而验证更大比例的依赖代码。
结论
发展趋势清晰可见：历史上仅适用于最高安全级别代码定制专家工作的正式验证，即将变得像今天的模糊测试一样，适用于几乎所有生产软件。正如静态类型和测试框架一样，验证将从“附加功能”演变为“内置特性”，这不仅由 LLM 驱动，也将受益于语言设计和开发工作流的创新。
在 LLM 自动扫描并发现越来越多代码漏洞的今天，必须采用能够保证代码安全属性的流程。LLM 规模化的正式验证是一种有前景的方法，能在以前无法企及的范围和规模上确保安全保证。鼓励开发者积极尝试，共同构建一个稳健软件普及、Bug 成为可快速解决之罕见现象的世界。
