We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that lift Rust into Lean 4; formal cryptographic specification libraries (ArkLib and CompPoly, from the Verified zkEVM project) that provide the mathematical targets; and AI provers (Aristotle from Harmonic AI and Aleph from Logical Intelligence) that close the resulting proof obligations. Every proof is checked by the Lean kernel, so AI output cannot compromise soundness. Within the scope of the Ethereum Foundation's zkEVM Verification Project, we applied the pipeline to cryptographic primitives in Plonky3 (FRI folding, Mersenne31 and KoalaBear field arithmetic, Horner polynomial evaluation) and RISC Zero (Merkle inclusion verification). In addition, Aleph authored proofs of two bounds-style theorems in Plonky3's compute_log_arity_for_round that previously stood as sorry. The paper describes the architecture, walks through a running example based on Aleph's two proofs, reports which classes of proof obligations AI closed and which required manual work, and discusses the engineering gaps we encountered: Lean 4 toolchain drift across tools and specific Aeneas/Hax extraction limits. We also document concrete missing lemmas, tactic gaps, and code-generation friction points discovered during proof development. We hope this contribution lowers the barrier to adoption of formal verification and facilitates more effective use of AI in this pipeline. The result is a working pipeline for formal verification of Rust, with kernel-checked proofs and reproducible artefacts.

翻译：我们描述了一条验证流水线，该流水线将生产级Rust密码学代码转化为Lean 4中经机器检查的正确性证明。该流水线整合了三个组件：符号提取工具（Charon和Aeneas，或Hax），将Rust提升到Lean 4；形式化密码学规范库（来自Verified zkEVM项目的ArkLib和CompPoly），提供数学目标；以及AI证明器（Harmonic AI的Aristotle和Logical Intelligence的Aleph），用于闭合由此产生的证明义务。每个证明均由Lean内核检查，因此AI输出不会损害可靠性。在以太坊基金会zkEVM验证项目的范围内，我们将该流水线应用于Plonky3（FRI折叠、Mersenne31和KoalaBear域算术、Horner多项式求值）和RISC Zero（Merkle包含验证）中的密码学原语。此外，Aleph还为Plonky3中`compute_log_arity_for_round`的两个界限式定理撰写了证明，这些定理此前被标记为`sorry`。本文描述了该架构，以Aleph的两个证明为基础示例进行讲解，报告了AI闭合了哪类证明义务、哪些需要人工操作，并讨论了我们遇到的技术缺口：跨工具的Lean 4工具链漂移以及特定的Aeneas/Hax提取限制。我们还记录了在证明开发过程中发现的具体缺失引理、策略缺口和代码生成摩擦点。我们希望这一贡献能降低形式化验证的采用门槛，并促进AI在此流水线中的更有效使用。最终成果是一条用于Rust形式化验证的可用流水线，包含内核检查的证明和可复现的工件。