一个使用AI证明器的Rust到Lean验证流水线：经验报告

# Rust到Lean的验证流水线：结合AI证明器的经验报告 来源：https://arxiv.org/html/2605.30106 Juan ConejeroPalina Tolmach Runtime Verification, Inc. \{nat.klaus, juan.conejero, palina.tolmach\}@runtimeverification.com (2026年5月) ###### 摘要 本文描述了一个验证流水线，该流水线能够将生产级Rust密码学代码转化为Lean 4中机器可验证的正确性证明。该流水线整合了三个组件：符号提取工具（Charon与Aeneas，或Hax）将Rust提升至Lean 4；形式化密码规范库（来自Verified zkEVM项目的ArkLib和CompPoly）提供数学目标；以及AI证明器（Harmonic AI的Aristotle和Logical Intelligence的Aleph）用于闭合由此产生的证明义务。每个证明均由Lean内核重新检查，因此AI输出不会破坏可靠性。在以太坊基金会zkEVM验证项目的范围内，我们将该流水线应用于Plonky3[19]（FRI折叠、Mersenne31和KoalaBear域运算、Horner多项式求值）和RISC Zero（Merkle包含验证）中的密码学原语。此外，Aleph为Plonky3的`compute_log_arity_for_round`中的两个边界型定理生成了证明，而这些定理此前被标记为`sorry`。本文描述了该架构，以Aleph的两个证明为运行示例进行详细说明，报告了哪些类别的证明义务由AI闭合、哪些需要人工介入，并讨论了我们遇到的技术差距：各工具间的Lean 4工具链漂移以及Aeneas/Hax特定的提取限制。我们还记录了在证明开发过程中发现的具体缺失引理、策略缺口和代码生成摩擦点。我们希望这项工作能降低形式化验证的采用门槛，并促进AI在该流水线中的更有效使用。其结果是一个可用于Rust形式化验证的工作流水线，具有内核检查的证明和可复现的制品。

## 1 引言

在生产协议栈中运行的密码学代码容错空间极小。FRI折叠中的一次错误会静默地破坏零知识虚拟机（zkVM）生成的每一个证明。Merkle包含检查中的一个漏洞会破坏所有依赖它的欺诈证明。代码审查、模糊测试和基于属性的测试各自能捕获一部分错误分布，但都有结构性限制。代码审查和基于属性的测试依赖于审计者或生成器预测正确的模式。模糊测试在输入空间上探索更广泛，但它在有限的输入预算下运行，且只能检测到可观察的失败，如崩溃、挂起或消毒器触发。满足这些信号的静默语义偏差可能不知不觉地通过。形式化验证则能生成覆盖所有输入的机器可检查证明，但仅针对工程师指定的属性。因此，规范设计成为一项核心工程活动，我们在第3节中讨论这一点。

形式化验证的成本历来是其障碍。标志性系统如seL4[15]和CompCert[17]已经证明，生产质量的软件可以完全验证，但每个系统都代表了在Isabelle/HOL或Rocq中多人年的努力，且证明与实现紧密耦合。对于Rust，最近的验证器如Verus[16]、Prusti[4]、Kani[27]和Creusot[10]通过将规范直接嵌入Rust源代码，并利用SMT求解器和模型检查自动化常见证明义务，降低了入门门槛。然而，它们针对语言的不同片段，解决不同的正确性问题，且没有一个能将生产级Rust与密码协议通常定义的抽象数学规范连接起来。

最近的三个发展共同大幅降低了工业形式化验证的成本。第一是Rust到证明助手的翻译工具集，它们保留了足够的源语义以支持真实验证：Aeneas[13]通过类型化的中间表示将安全Rust降低为纯函数式Lean 4；Hax[9]（Cryspen）是一种基于注解的替代方案，目标为Lean 4、F⋆和Rocq；以及rocq-of-rust[12]通过THIR将Rust翻译到Rocq。第二是AI证明器的出现，它们能够闭合交互式定理证明器中的非平凡证明义务：Harmonic AI的Aristotle[1]在2025年国际数学奥林匹克竞赛中报告了金牌级别的性能，而Logical Intelligence的Aleph在PutnamBench基准[14]上报告了99.4%的成绩。两者都生成Lean证明，内核重新检查这些证明，因此可靠性不依赖于AI的猜测是否正确。第三是Lean 4中形式化库的出现，使生产级验证变得实用。基础是Mathlib4，即社区维护的数学库[28]，以及CSLib[5]，这是一项近期努力，旨在为计算机科学做Mathlib为数学所做的事情。在这些基础之上，专门库为各个验证领域提供了抽象目标。与本工作最相关的两个库是ArkLib[25]（一个用于形式化验证SNARK协议的库，基于交互式预言机约简理论，包含Sum-Check、FRI、WHIR等形式化）和CompPoly[26]（一个用于计算多项式和有限域理论的库）。这些库共同提供了生产级Rust可以证明与之等价的抽象数学目标。

据我们所知，本文记录了首次尝试将这三个线索整合到单一流水线中，并应用于真实世界密码学Rust的工作。我们在以太坊基金会zkEVM验证项目下构建并运行了这样一个流水线，将其应用于Plonky3[19]和RISC Zero[20]中的密码学原语。本文做出四项贡献：
- **一个流水线。** 我们将符号Rust到Lean提取（Aeneas、Hax）、形式化密码规范库（ArkLib、CompPoly）和AI证明器（Aristotle、Aleph）集成到一个单一工作流中。
- **应用于密码学原语。** 我们将该流水线应用于Plonky3[19]和RISC Zero[20]中八个共识关键目标，涵盖有限域算术、FRI折叠与轮次调度、Horner多项式求值、Merkle包含验证以及位向量级别的32位ADC。所有代码、规范和证明都是公开的；主仓库位于https://github.com/Verified-zkEVM/rust-lean。
- **AI闭合证明的经验记录。** 我们在引理级别报告了Aleph自动闭合了哪些义务（`compute_log_arity_for_round`中的两个边界定理）以及每个证明使用的策略。
- **工程差距。** 我们记录了遇到的差距：各工具间的Lean 4工具链漂移，以及Aeneas和Hax中的特定提取限制。我们描述了实践中使用的两种可靠变通方法（在上游修复差距，并将函数重写为提取友好的模型），并简要讨论了分层工具化作为处理不安全Rust的方向，我们的流水线目前不覆盖这一点。

## 2 背景

本节介绍我们组合到流水线中的组件。熟悉Aeneas、Hax、Lean 4、ArkLib或AI证明器的读者可以跳过相应段落。

### 2.1 Charon与Aeneas

Charon[24]将安全Rust翻译为LLBC[13]，这是从Rust的MIR派生出的类型化中间表示。Aeneas[13]接受LLBC并生成纯函数式Lean 4代码。每个Rust函数都变为`Result α`单子中的一个Lean函数，其三个构造子`ok`、`fail`、`div`分别区分成功返回、恐慌和非终止。Aeneas使证明工程师免于基于内存的推理[13]：它将Rust的借用检查器保证视为语义输入。提取的Lean代码保持小巧，专注于功能性属性，可使用Mathlib4和Aeneas特定的策略（如`progress`和`scalar_tac`）进行证明。

### 2.2 Hax

Hax[9]是由Cryspen维护的Rust验证工具，它将Rust翻译为F⋆、Rocq、Lean和其他后端。其前端挂接到Rust编译器，并将THIR（类型化高级中间表示）导出为JSON；引擎随后通过基于注解的简化流水线进行降级。Lean 4后端目前正在积极开发中，而F⋆后端更为成熟。最近的独立分析[23]已识别出Hax提取与原始Rust语义之间针对某些Rust模式的语义差距；本文报告的验证工作限于纯的、有界循环函数片段，在这些片段中Hax的翻译是可靠的。

### 2.3 Lean 4与规范库

目标证明器是Lean 4，以Mathlib4作为其数学库。另外两个库提供了我们验证所依据的密码学规范：
ArkLib[25]形式化了简洁非交互知识论证（SNARK），即密码学证明系统，允许证明者说服验证者计算已正确执行，而无需验证者重新执行。ArkLib基于交互式预言机约简（IOR）理论，这是一种组合框架，其中复杂的证明系统被分解为一系列更简单的交互式协议，每个协议将一个关系约简为另一个关系[8]。该库包含Sum-Check、FRI、WHIR等协议在抽象层面的形式化，以及它们依赖的多项式机制（折叠、求值域）。
CompPoly[26]提供计算多项式和有限域理论，包括单变量、多变量和多线性多项式表示，以及与Mathlib代数类型的等价关系，既直接使用也作为ArkLib的基础。
两个库都是开源的，属于Verified zkEVM项目的一部分。作为本工作的一部分，我们已向上游两个库贡献了改进。

### 2.4 AI证明器

我们使用两个AI证明器作为Lean 4的外部证明搜索引擎。
Aristotle（Harmonic AI）[1]结合了Lean证明搜索系统与非形式化推理组件，后者生成并形式化候选引理。
Aleph（Logical Intelligence）[18]是一个用于定理证明的智能体编排层：它将证明义务分解为子问题（“规划”），为每个子问题生成Lean证明（“证明”），并根据哪些子部分成功来优化其策略（“优化”）。Aleph可以根据任务和资源预算与不同的底层推理模型配对。
Lean内核重新检查两个证明器发出的每个证明。

### 2.5 zkVM与Plonky3

零知识虚拟机（zkVM）在密码学证明系统内执行程序：VM生成一个简洁证明，表明执行是否正确，任何第三方无需重新执行程序即可验证该证明。RISC Zero[20]和SP1[22]是两个基于RISC-V指令集的生产级zkVM。两者都依赖于STARK证明系统[6]，其算术骨干由Plonky3[19]实现。
Plonky3[19]是一个开源的Rust工具包，用于构建STARK证明系统。它提供有限域实现（Mersenne31、BabyBear、KoalaBear）、快速里德-所罗门交互式预言机邻近证明（FRI）协议[6]以及zkVM依赖的多项式承诺基础设施。FRI是一种低度测试，允许验证者检查在有限域上求值的函数是否接近低度多项式。它通过对数数量的折叠轮次实现，每一轮将问题规模减半。这些组件中的任何错误，如错误的域乘法、不正确的FRI折叠步骤或有缺陷的Merkle包含检查，都会静默地使zkVM发出的每个证明无效。

Verified zkEVM项目[11]是一个多团队协作，旨在形式化验证整个栈中的组件。ArkLib和CompPoly（第2.3节）是该项目的一部分开发的。本文报告的验证工作也在同一项目下进行，以Plonky3和RISC Zero原语作为验证对象。

## 3 流水线架构

图1展示了数据流。流水线分四个阶段运行。

![图1：流水线数据流。提取（灰色）将Rust提升到Lean 4；规范（绿色）定义验证目标；证明（蓝色）由人工和AI辅助构建；Lean内核（红色）重新检查每个证明，构成信任边界。](https://arxiv.org/html/2605.30106/x1.png)

**图1：** 流水线数据流。提取（灰色）将Rust提升到Lean 4；规范（绿色）定义验证目标；证明（蓝色）由人工和AI辅助构建；Lean内核（红色）重新检查每个证明，构成信任边界。

#### 阶段 1：Rust到Lean 4。对于使用Aeneas的项目，我们在Cargo crate上运行Charon以生成LLBC文件，然后运行Aeneas将LLBC翻译为一对Lean文件（`Types.lean`和`Funs.lean`）。对于使用Hax的项目，我们使用`#[hax::contract]`及相关属性注解Rust项，然后运行`cargo hax into lean`。两种情况下，输出都是纯函数式Lean 4。Rust循环变为带有终止义务的递归函数。算术运算包裹在单子中（Aeneas为`Result α`，Hax为`RustM`），将溢出和恐慌路径暴露为显式失败情况。

#### 阶段 2：规范。规范来自两个来源。对于简单目标，我们针对提取的代码手动编写规范：一个镜像Rust计算的纯函数（在`N`或`Z/pZ`上），以及关于输入的前提条件（例如`p^2 ≤ 2^64 - 1`，或“所有输入小于p”）。对于匹配现有密码学抽象的目标，我们从ArkLib或CompPoly导入相关定义。