大多数软件充斥着漏洞，而人工智能如今能轻松发现并利用这些缺陷。传统的网络防御措施已显不足，业界亟需能够证明代码无漏洞的方法。形式化软件验证虽能提供此类保证，但历史上依赖专家耗时数年，难以在现实项目中普及。然而，在与 Theorem 的合作中，我们证实大语言模型（LLM）现已能大规模生成形式化证明，从而开启包含经证明安全保证的新软件开发工作流。
借助 Claude，我们在超过 100 个真实世界的开源软件库中，证明了汇编代码级别（RISC-V）的安全属性。据我们所知，这代表了首次大规模利用 AI 在生产软件的汇编代码层级应用形式化验证。在编写证明的过程中，Claude 还发现了多年来即便经过数万亿次测试运行仍未被检测到的漏洞。随着模型能力提升，我们预计形式化验证将成为安全软件开发的重要组成部分。
从测试到证明：重塑安全基准
即使是成熟且经过大量测试的软件也包含漏洞。Linux 内核最近披露了超过 1,000 个漏洞，随着前沿模型越来越擅长将看似无害的漏洞链式组合成关键利用程序，我们需要在野外被利用之前检测和修复这些漏洞的技术。
形式化验证通过将代码转换为数学模型，证明其始终遵循定义的安全规则。若无法证明，则暗示存在漏洞。然而，传统验证成本极高，例如 seL4 操作系统内核的开发耗时两人年，而验证却花了 20 人年，导致其仅适用于航电代码等任务关键型应用。
大语言模型改变了这一局面。我们要求 Claude 证明 123 个开源库中的安全属性，包括证明某些可执行工件在特定条件下永远不会崩溃。具体而言，Claude 证明了这些程序在所有输入小于 64 MB、且在 RISC-V CPU 上使用 Linux OS 作为单线程静态二进制文件运行的假设下，始终以正常方式退出，不触发内存安全错误或断言失败。
为解决规范定义难题，我们将现有的模糊测试（fuzz testing）套件转化为规范，编码规则为“此测试套件始终通过”。对于这个项目，我们从 Google 的 OSS-Fuzz 倡议中的数百个项目入手，将模糊测试转化为基于编译后 RISC-V 指令定义的规范：对于任何小于 64 MB 的输入，测试都不会崩溃。
在短短几周内，Claude 成功修补了它发现的漏洞，并证明了在 123 个不同的 OSS-Fuzz 库中的 239 个入口点上，对于任何输入（最多 64 MB）都没有崩溃。这些证明由约 1.8 亿行 Rocq 代码组成，典型的证明运行约 600,000 行，为中位长度为 18,000 条 RISC-V 指令的二进制文件提供安全保证。
发现并修复隐藏漏洞
尝试证明规范的过程发现了数百个漏洞。为了确保自动化流程无需人工干预，我们让 Claude 在发现漏洞后自动修补代码，重新生成规范并继续证明。
我们发现的大多数漏洞是传统模糊测试难以发现的。模糊测试通常限制输入大小（如 1 MB）并依赖代码覆盖率，而 Claude 在处理更大输入空间时展现了优势。例如，Claude 在一个解压程序中发现了一个计数器下溢，导致越界写入，但这仅在约 20 MB 且具有罕见特定布局的输入上发生。其他漏洞包括图像解码器中需要 64 MB 输入和超过 2 GB 内存的越界读取，以及 libexpat 中重新发现的 CVE-2026-56132。此外，Claude 还发现了从不崩溃的逻辑漏洞，如文件加载限制未被强制执行。
超越内存安全的验证案例
形式化验证的应用远不止于防止崩溃。我们还探索了其他验证场景：
- zlib 压缩算法：Claude 编写了 RFC 1950 的正式规范，并证明了 Linux 内核中的 zlib 实现正确实施了该规范。我们在 x86 编译的二进制文件上直接证明了这一属性，并在边缘情况中发现了一些次要的不可利用漏洞。
- Python 解释器：我们要求 Claude 在 Rust 中开发 Python 解释器的一个大子集，并使用 Verus 证明其符合 CPython 语义。实证测量显示，在超过 170 万个随机生成的 Python 程序中，99.95% 的测试行为与 CPython 一致。
- 关键应用漏洞挖掘：在验证一个广泛使用的 PDF 阅读器时，我们在一个星期内发现了与通常一年报告的同样多的安全漏洞，其中包括一个潜伏十多年的未知逻辑漏洞。
效率提升与未来展望
大语言模型辅助形式化验证的主要挑战在于证明可能需要数亿个令牌，成本高昂。但效率提升的迹象已经显现：
首先，新模型需要更少的令牌。Opus 5.5 在证明一半的任务时，比 Opus 5 少用了约 40% 的令牌。其次，证明具有可重用性。当代理共享工作区时，所需令牌比单独工作时少 17%。在 OSS-Fuzz 证明工作中，代理团队通过复制和适应其他团队的已完成证明，显著降低了重复工作量。
我们发布了本项目中尚未公开的可信组件（RISC-V 和 Linux 进程的形式模型、定理陈述及 Rocq 证明检查器），以及 Claude 针对部分模糊测试的完整 Rocq 证明。Theorem 也表示愿意为其他开源项目运行相同的管道，并发布了一项 Claude 技能以帮助开发人员开始验证自己的代码。
局限性与结论
必须明确，“形式化验证”并不等同于“无漏洞”。我们的证明基于特定的机器模型（单线程、静态 RISC-V 二进制文件、musl libc），而实际部署环境可能涉及 x86/ARM、动态链接 glibc 等差异。此外，规范可能未涵盖所有现实世界的交互，如调用者对库的误用。
尽管存在局限，轨迹依然清晰：历史上仅在最安全关键代码中实践的形式化验证，很快将像今天的模糊测试一样，对几乎所有生产软件都具有实用性。在大语言模型自动扫描并发现越来越多代码漏洞的今天，我们必须使用能够保证代码安全属性的流程。我们鼓励开发者探索与大语言模型结合的形式化验证，共同构建一个软件漏洞成为低概率事件的世界。