Claude 形式化验证深度解析：123 个开源库、239 个测试入口、Rocq 与 RISC-V 机器级安全证明

一、Claude 从生成代码走向证明代码

2026 年 10 月 22 日，Anthropic 发布了一项关于人工智能和软件形式化验证的重要研究。

在与 Theorem 合作的项目中，研究团队使用 Claude 为真实开源程序构造机器可检查的数学证明。

根据官方报告，研究覆盖 123 个开源库、239 个模糊测试入口，最终生成约 1.8 亿行 Rocq 证明代码。

这些证明针对经过编译的 RISC-V 程序，在指定假设下验证某些安全性质。

与传统 AI 编程展示不同，这项研究并不是让模型简单回答“代码看起来有没有问题”。

它要求模型提供足以让独立证明检查器接受的形式化证据。

也就是说，模型即使说得再有道理，如果证明不能通过检查，结果仍然不能被接受。

这种模式有望成为 AI 编程的重要补充：让生成代码与验证代码逐渐形成可审计的闭环。

但是，研究结论有严格适用范围。并非 123 个软件库中的所有代码、所有平台和所有功能都已被证明不存在漏洞。

二、形式化验证到底是什么？

形式化验证是通过数学模型和逻辑证明，判断一个程序是否满足明确指定的性质。

例如，普通单元测试可能检查：

输入为零时，程序是否返回预期结果。

输入为某个字符串时，程序是否正常结束。

但这些测试通常只覆盖有限数量的输入。

形式化验证则试图回答更一般的问题：

对于所有满足条件的输入，某项错误是否都不可能发生？

比如，在一个简化的数组处理程序中，可以尝试证明所有被访问的数组索引均处于合法范围。

这样的证明，不依赖只运行几个测试样例。

它需要描述程序的数学行为，并给出逻辑上可以成立的论证。

真正困难的地方在于，现实软件通常拥有庞大的执行状态空间，包含循环、内存、异常路径和外部系统调用。

因此，形式化验证过去往往需要专业人员投入大量时间。

三、为什么测试数量再多也无法替代数学证明？

传统软件测试能够发现问题，但无法轻易覆盖全部可能输入。

例如，一个图像解码器可能已经接受数万亿次模糊测试。

这并不意味着所有可能导致内存访问错误的图像文件都已经被尝试过。

输入文件可以具有不同长度、字节内容和复杂内部结构。

某些异常可能只有非常特殊的输入组合才会触发。

模糊测试也依赖输入生成策略和代码覆盖反馈。

因此，即使软件在长期测试中表现稳定，也可能仍然存在罕见缺陷。

形式化验证提供另一种思路。

它不是继续寻找更多测试输入，而是尝试证明：在定义好的输入范围和运行模型内，所有执行路径都满足目标性质。

这也是 Anthropic 认为该技术值得重新关注的原因。

四、Anthropic 的研究究竟证明了什么？

Anthropic 采用的主要方法，是把已经存在的 OSS-Fuzz 测试入口转化为形式化验证目标。

研究使用了 Google OSS-Fuzz 生态中的开源项目。

团队将相关测试程序编译为 RISC-V 可执行代码，并基于 RISC-V 指令和 Linux 进程模型构建数学语义。

证明目标大致可以理解为：

在给定运行假设下，对于小于 64 MB 的输入，程序不会因为指定的内存安全错误、断言失败等原因异常崩溃。

这并不是对整个软件的所有功能建立完整规格。

它首先针对的是测试入口能够表达的性质。

如果某个测试入口只验证程序不会发生特定类型的崩溃，那么证明也主要围绕这项性质展开。

因此，不能把“测试入口不会崩溃”直接翻译成“整个库没有任何安全漏洞”。

五、研究结果有哪些重要数字？

这些数字说明此次研究规模较大，但它们各自描述不同概念。

1.8 亿行代码是生成的证明代码量，不是被验证的软件源代码量。

239 个测试入口也不能理解为全部项目仅存在 239 条函数。

一个软件库可能具有很多功能，而研究只针对部分能够建立形式化目标的入口。

因此，引用数字时必须同时说明证明范围。

六、RISC-V 为什么出现在研究中？

RISC-V 是一种开放指令集架构。

软件源代码经过编译后，处理器实际执行的是相应架构的机器指令。

传统源代码层面的分析，可能需要对编译器行为作出额外假设。

而 Anthropic 此次主要研究直接对编译后的 RISC-V 指令建立证明。

这使验证对象更加接近最终执行程序。

不过，这并不代表任意 x86 或 ARM 版本的软件都会自然获得同样结论。

不同架构的指令、内存模型和系统行为可能不同。

要扩展至其他平台，需要为对应指令集和操作系统建立可信的形式语义。

因此，研究中使用 RISC-V 是一种明确的工程选择，而不是证明所有 CPU 上的程序都安全。

七、证明依赖哪些关键假设？

Anthropic 明确列出了限制条件。

研究中的主要证明以单线程、静态链接、固定内存预算的 RISC-V 程序为对象。

操作系统环境按照研究建立的 Linux 进程语义进行建模。

输入大小也有明确上限。

这些条件决定了证明的适用边界。

例如，如果程序在生产环境使用多个线程，可能引入并发竞争问题。

如果程序依赖动态库，实际执行环境也可能与被验证的静态程序不同。

如果输入超过所证明的大小上限，原有结论不能自动扩展到更大输入。

因此，形式化验证并不是脱离条件的绝对保证。

它真正提供的是：在明确条件下，对明确性质成立的严格证据。

八、Rocq 在研究中扮演什么角色？

Rocq 是著名的交互式证明系统，前身为 Coq。

开发者可以在其中表达定理、构造证明，再交由证明检查机制判断证明是否成立。

在此次研究中，Claude 负责生成大量证明代码。

Rocq 则负责对证明进行机器检查。

这意味着模型不再只是输出一份无法核查的自然语言解释。

研究人员可以通过严格的数学机制验证证明是否满足规格。

不过，证明检查器本身和输入的数学定义仍然属于需要信任的部分。

如果数学规格写错，证明可能正确地证明了一个没有实际价值的性质。

因此，证明代码通过检查，不等于研究者的业务需求被自动完整表达。

九、可信计算基础为什么重要？

Anthropic 将其研究依赖的可信部分归纳为几个关键对象。

包括 RISC-V 的形式语义、Linux 进程模型、被证明的具体定理陈述，以及 Rocq 证明检查器。

这些组件共同构成证明可信性的基础。

如果其中某个模型与真实硬件或操作系统行为存在差异，证明与实际运行结果之间也可能出现偏差。

这并不意味着形式化验证没有价值。

恰恰相反，它把需要审查的范围从庞大程序转移到数量相对有限的可信组件上。

对于长期维护的重要基础软件，这种结构具有很强的工程吸引力。

但可信组件仍然需要公开审查、测试和持续维护。

十、Claude 如何在证明过程中发现漏洞？

此次研究并非只有生成证明这一个成果。

Anthropic 表示，Claude 在尝试证明目标性质时，还发现了数百个缺陷。

其中部分问题存在于已经运行了极大量测试的开源项目中。

例如，研究提到某个解压缩相关程序只有在约 20 MB、具有特殊布局的输入下才会出现越界写入风险。

还包括图像解码器中的越界读取、复杂文件句柄调用顺序引起的问题，以及 libexpat 中与深层嵌套输入有关的已知漏洞重新发现。

这些案例显示，数学证明过程本身也可以成为寻找隐藏错误的方法。

因为一旦无法证明某条执行路径安全，模型就需要进一步理解原因。

但发现潜在问题与正式发布安全公告仍是不同步骤。

软件维护者需要独立确认、修复并按照负责任披露流程处理。

十一、为什么部分证明是在修补代码后完成的？

这一点非常关键。

Anthropic 并不是宣称原始的 239 个入口在研究开始时就全部安全。

在遇到能够导致目标性质失败的代码问题时，Claude 先尝试修复相关缺陷。

然后重新生成与修改后程序对应的证明任务，继续进行验证。

因此，最终被证明的程序版本可能已经不同于研究开始时的原始版本。

这也是为什么阅读形式化验证报告时，需要关注具体代码版本和证明对象。

不能在没有确认提交版本的情况下，将某份证明直接套用到其他发行版。

对于企业软件，证明与代码版本最好形成严格对应关系。

任何新的代码修改，都可能要求重新验证相关性质。

十二、能否证明不止内存安全这一种性质？

可以，但需要建立合适的数学规格。

Anthropic 还报告了对 zlib 压缩格式实现的进一步研究。

研究者尝试根据 RFC 1950 建立相关形式规格，并验证特定实现的行为。

此外，还开展了使用 Rust 实现 Python 解释器子集、验证其行为与 CPython 语义是否一致的实验。

在这一实验中，团队使用 Verus 等工具，并通过大量随机生成的 Python 程序进行额外比较。

这些探索显示，形式化方法可以处理一些功能正确性问题。

但它们属于不同实验，不能与 123 个开源库的 RISC-V 无崩溃证明混为一谈。

十三、形式化证明与自动化测试应当如何配合？

比较稳妥的工程方法，是把形式化验证加入现有开发流程，而不是立即移除全部传统测试。

例如，静态分析可以识别常见危险模式。

单元测试验证具体业务行为。

模糊测试探索异常输入。

形式化证明则尝试对关键性质建立更强的保证。

对于高风险系统，还需要代码审查、依赖安全检查和部署环境监控。

这种分层方法能够降低单一技术的盲点。

同时，企业可以优先选择范围明确、价值较高的模块试点。

例如，解析器、权限判断函数或关键状态机。

不必一开始就尝试证明整个业务系统的所有代码。

十四、形式化验证为什么长期难以普及？

主要障碍之一是成本。

证明一个复杂程序，可能需要编写比原程序长得多的逻辑描述和证明代码。

而且，开发人员还需要掌握特殊的数学工具和形式语言。

Anthropic 在报告中提到，seL4 微内核的开发与验证曾经需要大量专业工程投入。

大语言模型的出现，正在降低生成证明草稿和反复修复证明失败的人工成本。

但是模型计算成本本身仍然可能很高。

此次研究涉及数亿行证明输出，某些任务可能消耗大量 Token。

因此，大规模证明是否具有经济性，需要结合模型价格、执行时间和证明复用情况评估。

十五、Claude Opus 5.5 是否让证明更便宜？

Anthropic 还构建了 36 个较小的形式化验证任务，用于比较不同模型的工作效率。

官方称，在这些任务中，对于其中一半任务，Opus 5.5 相比 Opus 5 使用约少 40% 的 Token 完成证明。

这属于特定任务集中的观察结果。

不代表任何证明任务都能节省 40% 成本。

模型升级对证明成功率和计算资源的影响，还需要在更多不同项目上验证。

与此同时，Anthropic 发现，让多个 Agent 共享部分可复用证明，可以进一步减少重复工作。

这说明未来的效率提升，可能既来自更强模型，也来自更好的证明库和执行系统。

十六、开发者现在能使用哪些资源？

Anthropic 已经公开部分证明及相关形式语义，供研究人员独立验证和复用。

合作伙伴 Theorem 也公布了帮助开发者尝试形式化验证的相关工具与 Claude Skill。

但应当明确，这不是意味着 Claude 现已提供一个自动证明所有应用没有漏洞的正式在线产品。

开发者可以研究其公开流程，选择小范围模块试验。

真正用于生产级安全保证时，还需要检查模型假设、数学规格、证明版本和检查器环境。

【配图3：AI 辅助软件验证闭环。代码生成 → 单元测试 → 模糊测试 → 形式规格 → Rocq 证明 → 人工审查 → 持续集成。16:9。】

十七、这项研究对 AI 编程工具意味着什么？

AI 编程工具正在快速提高代码产出速度。

但如果代码生成数量增加，验证能力却没有同步提升，软件维护负担也可能增加。

因此，让 Agent 在生成代码后主动检查性质、运行测试和构建证明，将成为重要方向。

例如，编程 Agent 可以完成函数实现。

之后由测试工具检查常规行为。

再由证明工具验证指定边界条件。

最终交由人工审核。

这种方式能够提升结果可信度，但不能保证一切业务要求都能轻易形式化。

尤其是涉及用户体验、主观质量和复杂业务政策的需求，往往难以通过简单数学规格完整表达。

十八、常见问题 FAQ

Claude 已经证明 123 个库完全没有漏洞了吗？

没有。证明针对 239 个指定测试入口、输入大小、编译架构和运行假设。

1.8 亿行指的是开源软件代码吗？

不是，主要是生成的 Rocq 证明代码。

Rocq 是一个 AI 模型吗？

不是。它是用于构造和检查形式化数学证明的软件系统。

为什么需要 RISC-V？

研究选择在经过编译的 RISC-V 指令层面建立安全证明，不代表证明自动适用于所有 CPU 架构。

Claude 发现的漏洞是否都可直接利用？

不能这样判断。漏洞是否能在真实生产环境利用，需要具体确认。

这会替代单元测试和模糊测试吗？

短期内更适合形成互补关系。

普通开发者现在可以尝试吗？

可以研究公开证明资源和合作伙伴工具，但生产级验证仍需要专业工程审查。

十九、结语

Claude 形式化验证研究说明，AI 软件工程正在从快速生成代码，走向更严格的结果验证。

此次研究的真正突破，在于让模型承担过去需要大量专家时间的证明构造工作，并将最终正确性判断交给独立的机器检查机制。

但数学证明的力量来自明确的规格与假设，而不是来自模型的自信表达。

对于开发者来说，值得关注的是如何把自动化测试、模糊测试、形式化方法和人工审查组合起来。

未来，优秀的 AI 编程系统不仅要能够写出更多代码，还需要能够提供更可靠、更可审计的正确性证据。

官方来源

1. Anthropic — LLMs are making formal software verification feasible at a much larger scale https://www.anthropic.com/research/formal-verification

2. Theorem 官方网站 https://theorem.dev/

3. Google OSS-Fuzz 开源项目 https://github.com/google/oss-fuzz

4. Rocq 证明系统 https://rocq-prover.org/