Pith. sign in

REVIEW 2 major objections 2 minor 1 cited by

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report

T0 review · 2 major / 2 minor · reviewed 2026-06-29 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A pipeline lifts Rust cryptographic code into Lean 4 and uses AI provers to produce kernel-checked proofs.

desk verdict The paper shows AI provers closing two previously sorry bounds theorems in Plonky3 via a Rust-to-Lean pipeline, with kernel-checked results on several crypto primitives, but extraction semantics are assumed rather than checked. read the letter →

arxiv 2605.30106 v1 pith:GUEUFEFQ submitted 2026-05-28 cs.LO

Natalia Klaus , Palina Tolmach , Juan Conejero This is my paper · ORCID
classification cs.LO
keywords RustLean4formalverificationAIproverscryptographyPlonky3RISCZerosymbolicextraction
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper describes a verification pipeline that extracts production Rust code for cryptographic primitives into Lean 4 using symbolic tools, aligns the result with formal mathematical specifications, and relies on AI provers to discharge proof obligations that the Lean kernel then checks for soundness. It applies this process to FRI folding, field arithmetic, Horner evaluation from Plonky3 and Merkle inclusion from RISC Zero. The pipeline also yields AI-generated proofs for two bounds-style theorems that had remained as sorry statements. The work reports the architecture, a running example, the split between automated and manual proof work, and specific engineering limitations encountered.

What carries the argument

The three-stage pipeline of symbolic extraction tools (Charon, Aeneas or Hax) that lift Rust into Lean 4, formal cryptographic specification libraries (ArkLib and CompPoly) that supply the mathematical targets, and AI provers (Aristotle and Aleph) that close obligations, all under Lean kernel checking.

What would settle it

An input on which the extracted Lean version of a verified Plonky3 or RISC Zero function produces a different result from the original Rust implementation.

Watch

Extended reading notes

Core claim

The pipeline produces machine-checked Lean 4 proofs for cryptographic primitives in Plonky3 (FRI folding, Mersenne31 and KoalaBear field arithmetic, Horner polynomial evaluation) and RISC Zero (Merkle inclusion verification), and Aleph authored proofs of two bounds-style theorems in compute_log_arity_for_round that previously stood as sorry.

Load-bearing premise

The symbolic extraction tools preserve the semantics of the original Rust code without introducing mismatches that would invalidate the subsequent proofs.

Editorial extensions

If this is right

  • Machine-checked proofs now exist for the listed Plonky3 and RISC Zero primitives.
  • Two previously sorry bounds theorems in compute_log_arity_for_round have machine-checked Lean proofs.
  • AI provers closed certain classes of obligations while others still required manual intervention.
  • The pipeline surfaces concrete gaps such as Lean 4 toolchain drift and extraction limits in Aeneas and Hax.
  • Missing lemmas and tactic gaps are documented for future work on the same primitives.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same extraction-plus-AI pattern could be tested on additional Rust cryptographic libraries beyond the two projects named.
  • If extraction fidelity improves, the fraction of obligations closed by AI without manual help would likely rise.
  • Reproducing the pipeline on a different formal system would test whether the reported engineering gaps are Lean-specific.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 2 minor

Summary. This experience report describes a verification pipeline that uses symbolic extraction tools (Charon, Aeneas, or Hax) to lift production Rust cryptographic code into Lean 4, combines it with formal specifications from ArkLib and CompPoly, and employs AI provers (Aristotle and Aleph) to generate proofs that are ultimately checked by the Lean kernel. The pipeline is applied to primitives in Plonky3 (FRI folding, field arithmetic, Horner evaluation) and RISC Zero (Merkle inclusion), and Aleph is used to prove two bounds theorems in compute_log_arity_for_round that were previously sorry.

Significance. If the extraction semantics are preserved, the work provides a concrete, reproducible demonstration of integrating AI provers into a formal verification pipeline for real cryptographic Rust code from Plonky3 and RISC Zero, with all final proofs kernel-checked by Lean and with explicit documentation of which obligation classes were AI-closed versus manually completed. The reported engineering gaps, missing lemmas, and toolchain issues constitute useful practical data for the zkEVM verification community.

major comments (2)
  1. [Pipeline architecture description] The central claim that the pipeline 'takes production Rust cryptographic code and produces machine-checked correctness proofs' for the original Rust (FRI folding, field arithmetic, Horner evaluation, Merkle inclusion, and the two bounds theorems) depends on faithful semantic preservation by the extraction step. The manuscript describes the architecture and extraction limits but supplies no equivalence argument, manual cross-check, or diff against the Rust source for any of the concrete extractions used.
  2. [Abstract] The abstract states that the body 'reports which classes of proof obligations AI closed and which required manual work' yet provides no quantitative breakdown (e.g., counts or percentages per primitive) of success rates; this weakens the empirical contribution even though the soundness of the final Lean proofs is not in question.
minor comments (2)
  1. Consider adding a summary table that lists each target primitive, the extraction tool used, the number of obligations, and the resolution method (AI vs. manual) to make the reported experience more immediately usable.
  2. The discussion of 'Lean 4 toolchain drift across tools' would benefit from a short enumerated list of the specific version incompatibilities encountered.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. Below we provide point-by-point responses to the major comments and indicate the revisions we plan to make.

read point-by-point responses

  1. Referee: [Pipeline architecture description] The central claim that the pipeline 'takes production Rust cryptographic code and produces machine-checked correctness proofs' for the original Rust (FRI folding, field arithmetic, Horner evaluation, Merkle inclusion, and the two bounds theorems) depends on faithful semantic preservation by the extraction step. The manuscript describes the architecture and extraction limits but supplies no equivalence argument, manual cross-check, or diff against the Rust source for any of the concrete extractions used.

    Authors: The referee correctly identifies that the manuscript does not supply an equivalence argument or cross-checks for the extraction. Our work is an experience report on the use of AI provers within the pipeline, and we take the semantic preservation of Charon, Aeneas, and Hax as given by their developers. We will revise the manuscript to include an explicit statement of this assumption and a discussion of the extraction limits in a new subsection. This will clarify the scope without claiming full semantic equivalence proofs, which are beyond the paper's contribution. revision: partial

  2. Referee: [Abstract] The abstract states that the body 'reports which classes of proof obligations AI closed and which required manual work' yet provides no quantitative breakdown (e.g., counts or percentages per primitive) of success rates; this weakens the empirical contribution even though the soundness of the final Lean proofs is not in question.

    Authors: We agree that a quantitative breakdown would enhance the empirical value of the report. Although the manuscript describes the classes of obligations qualitatively, we will add quantitative data in the revised version, including a table with counts of AI-closed versus manually completed obligations for each primitive. The abstract will be updated accordingly to reflect this addition. revision: yes

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: empirical experience report with no derivation chain

full rationale

The paper is an experience report on applying a Rust-to-Lean pipeline to cryptographic code. It contains no mathematical derivations, fitted parameters presented as predictions, uniqueness theorems, or ansatzes. All central claims are observational reports of tool outputs and proof closures, with kernel-checked Lean proofs as the external benchmark. No step reduces to its own inputs by construction or self-citation. The noted semantic-preservation assumption is an engineering limitation, not a load-bearing derivation.

Assumptions & free parameters 0 free parameters · 0 assumptions · 0 invented entities

As an experience report on tool integration rather than a mathematical derivation, the paper introduces no free parameters, axioms, or invented entities.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report." pith.science (2026). https://pith.science/paper/GUEUFEFQ

@misc{pith2026260530106,
  author       = {Pith},
  title        = {Pith review of: A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GUEUFEFQ}},
  note         = {Machine review of arXiv:2605.30106}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2605.30106 by the authors.

Figure 1
Figure 1. Pipeline data flow. Extraction (grey) lifts Rust into Lean 4; specifications (green) [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. An AI Approach to Verified Production Cryptographic Libraries

    cs.CR 2026-08 conditional novelty 6.0 of 10

    An AI agent, guarded by mechanical integrity gates, synthesized Verus-verified internal specifications and proofs for curve25519-dalek and chacha20 without changing executable code.

Reference graph

Works this paper leans on

31 extracted references · cited by 1 Pith paper

  1. [1]

    Aristotle: IMO-level automated theorem proving, 2025

    Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, et al. Aristotle: IMO-level automated theorem proving, 2025

    2025

  2. [2]

    Proof forarity_respects_max_bound, PR #1.https://github.com/r untimeverification/p3-hax-lean-fri-pipeline/pull/1, 2026

    Aleph Prover Bot. Proof forarity_respects_max_bound, PR #1.https://github.com/r untimeverification/p3-hax-lean-fri-pipeline/pull/1, 2026. 12

    2026

  3. [3]

    Proof forarity_respects_target_distance, PR #3.https://github .com/runtimeverification/p3-hax-lean-fri-pipeline/pull/3, 2026

    Aleph Prover Bot. Proof forarity_respects_target_distance, PR #3.https://github .com/runtimeverification/p3-hax-lean-fri-pipeline/pull/3, 2026

    2026

  4. [4]

    Vytautas Astrauskas, Aurel Bílý, Jonas Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers. The Prusti Project: Formal verification for Rust. InNASA Formal Methods (NFM), pages 88–108, 2022

    2022

  5. [5]

    CSLib: The Lean Computer Science Library, 2026

    Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, and Sorrachai Yingchareonthawornchai. CSLib: The Lean Computer Science Library, 2026

    2026

  6. [6]

    Scalable, transparent, and post-quantum secure computational integrity

    Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev. Scalable, transparent, and post-quantum secure computational integrity. IACR Cryptology ePrint Archive, 2018/046, 2018

    2018

  7. [7]

    Signal Shot: end-to-end formal verification of the Signal protocol

    Beneficial AI Foundation. Signal Shot: end-to-end formal verification of the Signal protocol. https://www.beneficialaifoundation.org/blog/signal-shot, 2026

    2026

  8. [8]

    Alessandro Chiesa, Yuncong Hu, Mary Maller, Pratyush Mishra, Noah Vesely, and Nicholas P. Ward. Marlin: Preprocessing zkSNARKs with universal and updatable SRS. IACR Cryptology ePrint Archive, 2019/1047, 2019

    2019

Show all 31 references
  1. [9]

    Hax: Verification-friendly Rust subset.https://github.com/cryspen/hax, 2024

    Cryspen. Hax: Verification-friendly Rust subset.https://github.com/cryspen/hax, 2024

    2024

  2. [10]

    Creusot: A foundry for the deductive verification of Rust programs

    Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A foundry for the deductive verification of Rust programs. InInternational Conference on Formal Engineering Methods (ICFEM), 2022

    2022

  3. [11]

    zkEVM Verification Project

    Ethereum Foundation. zkEVM Verification Project. https://github.com/Verified- zkEVM/, 2025

    2025

  4. [12]

    rocq-of-rust.https://github.com/formal-land/rocq-of-rust, 2024

    Formal Land. rocq-of-rust.https://github.com/formal-land/rocq-of-rust, 2024

    2024

  5. [13]

    Aeneas: Rust verification by functional translation

    Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proceedings of the ACM on Programming Languages, 6(ICFP):711–741, 2022

    2022

  6. [14]

    Logical Intelligence’s Aleph Solves PutnamBench

    Vlad Isenbaev and Boris Hanin. Logical Intelligence’s Aleph Solves PutnamBench. Logical Intelligence Blog, 2026

    2026

  7. [15]

    seL4: Formal verification of an OS kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd A...

    2009

  8. [16]

    Verus: Verifying Rust programs using linear ghost types

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. InProceedings of the ACM on Programming Languages, OOPSLA, 2023

    2023

  9. [17]

    Formal verification of a realistic compiler.Communications of the ACM, 52(7):107–115, 2009

    Xavier Leroy. Formal verification of a realistic compiler.Communications of the ACM, 52(7):107–115, 2009

    2009

  10. [18]

    Aleph Prover.https://logicalintelligence.com/aleph-prover.h tml, 2025

    Logical Intelligence. Aleph Prover.https://logicalintelligence.com/aleph-prover.h tml, 2025. Accessed 2026-05-22

    2025

  11. [19]

    Plonky3: High-performance polynomial commitment and proof system

    Polygon Zero. Plonky3: High-performance polynomial commitment and proof system. https://github.com/Plonky3/Plonky3, 2024. 13

    2024

  12. [20]

    RISC Zero: zero-knowledge virtual machine for general Rust programs

    RISC Zero, Inc. RISC Zero: zero-knowledge virtual machine for general Rust programs. https://github.com/risc0/risc0, 2024

    2024

  13. [21]

    Towards large language models as copilots for theorem proving in Lean, 2024

    Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean, 2024

    2024

  14. [22]

    SP1: zkVM.https://github.com/succinctlabs/sp1, 2024

    Succinct Labs. SP1: zkVM.https://github.com/succinctlabs/sp1, 2024

    2024

  15. [23]

    The Verification Facade: Structural Gaps in Cryspen’s Hax Pipeline

    Symbolic Software. The Verification Facade: Structural Gaps in Cryspen’s Hax Pipeline. Symbolic Software Blog, 2026

    2026

  16. [24]

    Charon: Rust to LLBC translator.https://github.com/AeneasVer if/charon, 2024

    The Aeneas Project. Charon: Rust to LLBC translator.https://github.com/AeneasVer if/charon, 2024

    2024

  17. [25]

    ArkLib: Formal verification of cryptographic protocols in Lean 4

    The ArkLib Team. ArkLib: Formal verification of cryptographic protocols in Lean 4. https://github.com/Verified-zkEVM/ArkLib, 2025

    2025

  18. [26]

    CompPoly: Computational polynomial theory in Lean 4.https: //github.com/Verified-zkEVM/CompPoly, 2025

    The CompPoly Team. CompPoly: Computational polynomial theory in Lean 4.https: //github.com/Verified-zkEVM/CompPoly, 2025

    2025

  19. [27]

    Kani Rust Verifier.https://github.com/model-checking/kani, 2024

    The Kani Team. Kani Rust Verifier.https://github.com/model-checking/kani, 2024

    2024

  20. [28]

    mathlib4.https://github.com/leanprover-community/math lib4, 2024

    The mathlib Community. mathlib4.https://github.com/leanprover-community/math lib4, 2024

    2024

  21. [29]

    cargo-anneal: Specifications and soundness proofs for unsafe Rust

    The zerocopy Authors. cargo-anneal: Specifications and soundness proofs for unsafe Rust. https://crates.io/crates/cargo-anneal, 2026

    2026

  22. [30]

    Trinh, Yuhuai Wu, Quoc V

    Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. DeepMind blog and Nature publication, 2024

    2024

  23. [31]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. InNeurIPS, 2023. 14

    2023

Pith tools

Reviewed June 29, 2026 · model on record in the stance chip above.