A Rust-to-Lean verification pipeline with AI provers: An experience report

# A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Source: [https://arxiv.org/html/2605.30106](https://arxiv.org/html/2605.30106)
Juan ConejeroPalina Tolmach Runtime Verification, Inc\. \{nat\.klaus, juan\.conejero, palina\.tolmach\}@runtimeverification\.com

\(May 2026\)

###### 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\[[19](https://arxiv.org/html/2605.30106#bib.bib17)\]\(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’scompute\_log\_arity\_for\_roundthat previously stood assorry\.

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\.

## 1Introduction

Cryptographic code that runs inside production protocol stacks tolerates very few mistakes\. A bug in one round of FRI folding silently corrupts every proof a zero\-knowledge virtual machine \(zkVM\) emits\. A bug in a Merkle inclusion check breaks every fraud proof that depends on it\. Code review, fuzzing, and property\-based testing each catch a different slice of the bug distribution, but each has structural limits\. Code review and property\-based testing depend on the auditor or generator anticipating the right patterns\. Fuzzing explores inputs more broadly, but it runs on a finite input budget and detects only observable failures such as crashes, hangs, or sanitizer trips\. Silent semantic divergences that satisfy these signals can pass through unnoticed\. Formal verification produces a machine\-checked proof covering every input, but only against the property the engineer has specified\. Specification design therefore becomes a central engineering activity, and one we discuss in Section[3](https://arxiv.org/html/2605.30106#S3)\.

The cost of formal verification has historically been the obstacle\. Landmark systems such as seL4\[[15](https://arxiv.org/html/2605.30106#bib.bib22)\]and CompCert\[[17](https://arxiv.org/html/2605.30106#bib.bib23)\]demonstrated that production\-quality software can be fully verified, but each represents many person\-years of effort in Isabelle/HOL or Rocq, with proofs developed in close coupling to the implementation\. For Rust specifically, recent verifiers such as Verus\[[16](https://arxiv.org/html/2605.30106#bib.bib24)\], Prusti\[[4](https://arxiv.org/html/2605.30106#bib.bib25)\], Kani\[[27](https://arxiv.org/html/2605.30106#bib.bib26)\], and Creusot\[[10](https://arxiv.org/html/2605.30106#bib.bib27)\]have lowered the entry barrier by embedding specifications directly in Rust source code and automating common proof obligations through SMT solvers and model checking\. However, they target different fragments of the language and address different correctness questions, and none of them connects production Rust to the kind of abstract mathematical specifications that cryptographic protocols are usually defined against\.

Three recent developments together lower the cost of industrial formal verification substantially\. The first is a set of Rust\-to\-proof\-assistant translation tools that preserve enough of the source semantics to support real verification: Aeneas\[[13](https://arxiv.org/html/2605.30106#bib.bib1)\]lowers safe Rust into pure functional Lean 4 via a typed intermediate representation; Hax\[[9](https://arxiv.org/html/2605.30106#bib.bib6)\]\(Cryspen\) is an annotation\-driven alternative targeting Lean 4, F⋆, and Rocq; and rocq\-of\-rust\[[12](https://arxiv.org/html/2605.30106#bib.bib9)\]translates Rust into Rocq via THIR\.

The second is the emergence of AI provers that can close non\-trivial proof obligations in interactive theorem provers: Aristotle\[[1](https://arxiv.org/html/2605.30106#bib.bib2)\]from Harmonic AI reports gold\-medal\-equivalent performance on the 2025 International Mathematical Olympiad, and Aleph from Logical Intelligence reports 99\.4% on the PutnamBench benchmark\[[14](https://arxiv.org/html/2605.30106#bib.bib5)\]\. Both produce Lean proofs that the kernel re\-checks, so soundness does not depend on whether the AI guessed correctly\.

The third is the appearance of formal libraries in Lean 4 that make production verification practical\. The foundation is Mathlib4, the community\-maintained mathematical library\[[28](https://arxiv.org/html/2605.30106#bib.bib11)\], and CSLib\[[5](https://arxiv.org/html/2605.30106#bib.bib12)\], a recent effort to do for computer science what Mathlib does for mathematics\. Building on these foundations, specialised libraries provide the abstract targets for individual verification domains\. The two most relevant to this work are ArkLib\[[25](https://arxiv.org/html/2605.30106#bib.bib13)\], a library for formally verifying SNARK protocols built on the theory of Interactive Oracle Reductions \(with formalisations of Sum\-Check, FRI, WHIR, and others\), and CompPoly\[[26](https://arxiv.org/html/2605.30106#bib.bib14)\], a library for computational polynomial and finite\-field theory\. Together, these libraries provide the abstract mathematical targets that production Rust can be proved equivalent to\.

To the best of our knowledge, this paper documents the first attempt to combine these three threads in a single pipeline and apply it to real\-world cryptographic Rust\. We built and operated such a pipeline under the Ethereum Foundation’s zkEVM Verification Project, applying it to cryptographic primitives in Plonky3\[[19](https://arxiv.org/html/2605.30106#bib.bib17)\]and RISC Zero\[[20](https://arxiv.org/html/2605.30106#bib.bib18)\]\.

This paper makes four contributions:

- •*A pipeline\.*We integrate symbolic Rust\-to\-Lean extraction \(Aeneas, Hax\), formal cryptographic specification libraries \(ArkLib, CompPoly\), and AI provers \(Aristotle, Aleph\) into a single workflow\.
- •*Application to cryptographic primitives\.*We apply the pipeline to eight consensus\-critical targets across Plonky3\[[19](https://arxiv.org/html/2605.30106#bib.bib17)\]and RISC Zero\[[20](https://arxiv.org/html/2605.30106#bib.bib18)\], spanning finite\-field arithmetic, FRI folding and round\-scheduling, Horner polynomial evaluation, Merkle inclusion verification, and a 32\-bit ADC at the bit\-vector level\. All code, specifications, and proofs are public; the main repository is[https://github\.com/Verified\-zkEVM/rust\-lean](https://github.com/Verified-zkEVM/rust-lean)\.
- •*An empirical account of AI\-closed proofs\.*We report at the lemma level which obligations Aleph closed automatically \(two bounds theorems incompute\_log\_arity\_for\_round\) and the proof strategy each used\.
- •*Engineering gaps\.*We document the gaps we encountered: Lean 4 toolchain drift across tools, and specific extraction limits in Aeneas and Hax\. We describe two reliable workarounds we used in practice \(fixing the gap upstream and rewriting the function as an extraction\-friendly model\) and briefly discuss layered tooling as a direction for unsafe Rust, which our pipeline does not currently cover\.

## 2Background

This section introduces the components we compose into the pipeline\. Readers familiar with Aeneas, Hax, Lean 4, ArkLib, or the AI provers can skip the corresponding paragraphs\.

### 2\.1Charon and Aeneas

Charon\[[24](https://arxiv.org/html/2605.30106#bib.bib8)\]translates safe Rust into LLBC\[[13](https://arxiv.org/html/2605.30106#bib.bib1)\], a typed intermediate representation derived from Rust’s MIR\. Aeneas\[[13](https://arxiv.org/html/2605.30106#bib.bib1)\]takes LLBC and produces pure functional Lean 4 code\. Each Rust function becomes a Lean function in theResultα\\alphamonad, whose three constructorsok,fail,divdistinguish successful return, panic, and non\-termination\.

Aeneas relieves the proof engineer of memory\-based reasoning\[[13](https://arxiv.org/html/2605.30106#bib.bib1)\]: it treats Rust’s borrow\-checker guarantees as a semantic input\. The extracted Lean code stays small and focused on functional properties, provable with Mathlib4 and Aeneas\-specific tactics such asprogressandscalar\_tac\.

### 2\.2Hax

Hax\[[9](https://arxiv.org/html/2605.30106#bib.bib6)\]is a Rust verification tool maintained by Cryspen that translates Rust into F⋆, Rocq, Lean, and other backends\. Its frontend hooks into the Rust compiler and exports the THIR \(Typed High\-level Intermediate Representation\) as JSON; the engine then lowers this through an annotation\-driven simplification pipeline\. The Lean 4 backend is currently under active development, while the F⋆backend is more mature\.

Recent independent analysis\[[23](https://arxiv.org/html/2605.30106#bib.bib7)\]has identified semantic gaps between Hax extractions and the original Rust semantics for certain Rust patterns; the verification work reported here stays within the fragment of pure, bounded\-loop functions where Hax’s translation is reliable\.

### 2\.3Lean 4 and the spec libraries

The target prover is Lean 4 with Mathlib4 as its mathematical library\. Two further libraries provide the cryptographic specifications we verify against:

ArkLib\[[25](https://arxiv.org/html/2605.30106#bib.bib13)\]formalises succinct non\-interactive arguments of knowledge \(SNARKs\), cryptographic proof systems that allow a prover to convince a verifier that a computation was performed correctly without the verifier re\-executing it\. ArkLib builds on the theory of Interactive Oracle Reductions \(IORs\), a compositional framework in which a complex proof system is decomposed into a sequence of simpler interactive protocols, each reducing one relation to another\[[8](https://arxiv.org/html/2605.30106#bib.bib21)\]\. The library includes formalisations of Sum\-Check, FRI, WHIR, and other protocols at the abstract level, together with the polynomial machinery \(folding, evaluation domains\) they depend on\.

CompPoly\[[26](https://arxiv.org/html/2605.30106#bib.bib14)\]provides computational polynomial and finite\-field theory, including univariate, multivariate, and multilinear polynomial representations with equivalences to Mathlib’s algebraic types, used both directly and as a foundation under ArkLib\.

Both libraries are open\-source and part of the Verified zkEVM project\. As part of this work, we have contributed upstream improvements to both libraries\.

### 2\.4AI provers

We use two AI provers as external proof\-search engines for Lean 4\. Aristotle \(Harmonic AI\)\[[1](https://arxiv.org/html/2605.30106#bib.bib2)\]combines a Lean proof\-search system with an informal reasoning component that generates and formalises candidate lemmas\. Aleph \(Logical Intelligence\)\[[18](https://arxiv.org/html/2605.30106#bib.bib4)\]is an agentic orchestration layer for theorem proving: it decomposes a proof obligation into subproblems \(“planning”\), generates Lean proofs for each \(“proving”\), and refines its strategy based on which subparts succeed \(“refining”\)\. Aleph can be paired with different underlying reasoning models depending on the task and resource budget\. The Lean kernel re\-checks every proof both provers emit\.

### 2\.5zkVMs and Plonky3

Zero\-knowledge virtual machines \(zkVMs\) execute programs inside a cryptographic proof system: the VM produces a succinct proof that the execution was correct, which any third party can verify without re\-executing the program\. RISC Zero\[[20](https://arxiv.org/html/2605.30106#bib.bib18)\]and SP1\[[22](https://arxiv.org/html/2605.30106#bib.bib19)\]are two production zkVMs built on the RISC\-V instruction set\. Both rely on STARK proof systems\[[6](https://arxiv.org/html/2605.30106#bib.bib20)\]whose arithmetic backbone is implemented in Plonky3\[[19](https://arxiv.org/html/2605.30106#bib.bib17)\]\.

Plonky3\[[19](https://arxiv.org/html/2605.30106#bib.bib17)\]is an open\-source Rust toolkit for building STARK proof systems\. It provides finite field implementations \(Mersenne31, BabyBear, KoalaBear\), the Fast Reed\-Solomon Interactive Oracle Proof of Proximity \(FRI\) protocol\[[6](https://arxiv.org/html/2605.30106#bib.bib20)\], and the polynomial commitment infrastructure that zkVMs build on\. FRI is a low\-degree test that lets a verifier check whether a function evaluated over a finite field is close to a low\-degree polynomial\. It does so through a logarithmic number of folding rounds, each reducing the problem size by half\. A bug in any of these components, such as a wrong field multiplication, an incorrect FRI folding step, or a flawed Merkle inclusion check, silently invalidates every proof the zkVM emits\.

The Verified zkEVM project\[[11](https://arxiv.org/html/2605.30106#bib.bib34)\]is a multi\-team effort to formally verify components across this stack\. ArkLib and CompPoly \(Section[2\.3](https://arxiv.org/html/2605.30106#S2.SS3)\) were developed as part of this project\. The verification work reported in this paper was carried out under the same project, targeting Plonky3 and RISC Zero primitives as verification subjects\.

## 3Pipeline Architecture

Figure[1](https://arxiv.org/html/2605.30106#S3.F1)shows the data flow\. The pipeline runs in four stages\.

Rust crate\(Plonky3, RISC Zero, …\)Charon\(Rust→\\toLLBC\)Aeneas / Hax\(LLBC→\\toLean 4\)Lean 4 extracted codeTheorem statementProof constructionLean 4 kernelre\-checks every proofMachine\-checked theoremsSpecificationsHandwritten specsArkLib / CompPolyManual proofAI provers\(Aristotle, Aleph\)Figure 1:Pipeline data flow\. Extraction \(grey\) lifts Rust into Lean 4; specifications \(green\) define the verification targets; proofs \(blue\) are constructed manually and with AI assistance; the Lean kernel \(red\) re\-checks every proof, constituting the trust boundary\.#### Stage 1: Rust to Lean 4\.

For projects using Aeneas, we run Charon on the Cargo crate to produce an LLBC file, then run Aeneas to translate LLBC into a pair of Lean files \(Types\.leanandFuns\.lean\)\. For projects using Hax, we annotate Rust items with\#\[hax::contract\]and related attributes, then runcargo hax into lean\.

In both cases, the output is pure functional Lean 4\. Rust loops become recursive functions with termination obligations\. Arithmetic operations are wrapped in monads \(Resultα\\alphafor Aeneas,RustMfor Hax\) that expose overflow and panic paths as explicit failure cases\.

#### Stage 2: Specification\.

Specifications come from two sources\. For simple targets, we write them by hand against the extracted code: a pure function \(overℕ\\mathbb\{N\}orℤ/p​ℤ\\mathbb\{Z\}/p\\mathbb\{Z\}\) that mirrors the Rust computation, together with preconditions on the inputs \(for example,p2≤264−1p^\{2\}\\leq 2^\{64\}\-1, or “all inputs are less thanpp”\)\. For targets that match an existing cryptographic abstraction, we import the relevant definition from ArkLib or CompPoly and state the spec as equivalence to that definition\. The FRI fold example in Section[4](https://arxiv.org/html/2605.30106#S4)takes this second route: the Rust output is proved equal to one evaluation of ArkLib’sfoldNth 2 fβ\\betapolynomial fold\.

The main theorem of each verification target then states: under the precondition structure, the extracted Rust function returns a value matching the specification\.

#### Stage 3: Proof\.

Proofs are constructed either manually or with the help of AI provers, and typically combine both\. The available automation includes:

- •Aeneas\-specific tactics \(when extraction goes through Aeneas\):progresssteps through monadiclet x←\\leftarrowebindings and closes “operation succeeds” obligations using preconditions in context;scalar\_tacdischarges integer\-bound side conditions\.
- •General Lean 4 tactics:omega\(linear arithmetic\),nlinarith\(nonlinear bounds\),ring\(algebraic identities\),simp\(rewriting\), anddecide\(decidable propositions\)\. These come from Lean 4 core and Mathlib4\.
- •AI provers: Aristotle and Aleph can be invoked to close individual lemmas or whole theorems\. Section[5](https://arxiv.org/html/2605.30106#S5)gives an empirical account of which classes of obligation they handle well\.

Manual and AI\-driven proofs coexist in the same Lean file\. There is no semantic distinction between them at the kernel level\.

#### Stage 4: Re\-check\.

The Lean kernel re\-checks every proof, constituting the trust boundary of the described pipeline: regardless of whether a proof was written by a human, generated by an AI prover, or assembled from automated tactics, the kernel accepts it only if it typechecks\.

## 4Running Example:compute\_log\_arity\_for\_round

We use Plonky3’scompute\_log\_arity\_for\_round, an FRI\[[6](https://arxiv.org/html/2605.30106#bib.bib20)\]round\-scheduling function fromfri/src/config\.rs, as the running example\. The function decides how aggressively a given FRI round folds, subject to three constraints: a maximum allowed arity, the distance to the final target height, and the distance to the next input commitment\.

The Plonky3 source, lightly elided:

1pubfncompute\_log\_arity\_for\_round\(

2log\_current\_height:usize,

3next\_input\_log\_height:Option<usize\>,

4log\_final\_height:usize,

5max\_log\_arity:usize,

6\)\-\>RustM<usize\>\{

7letmax\_fold\_to\_target=log\_current\_height\-log\_final\_height;

8letmax\_fold=matchnext\_input\_log\_height\{

9None=\>max\_fold\_to\_target,

10Some\(next\)=\>\{

11letto\_next=log\_current\_height\-next;

12ifto\_next<max\_fold\_to\_target\{to\_next\}else\{max\_fold\_to\_target\}

13\}

14\};

15ifmax\_fold<max\_log\_arity\{max\_fold\}else\{max\_log\_arity\}

16\}

Hax extracts this into Lean 4, wrapping each checked subtraction in aRustMmonad and representing each conditional as a Leanif/then/else\. We can formulate two theorems: the result must not exceed the maximum allowed arity \(arity\_respects\_max\_bound\), and the result must not exceed the distance to the final height \(arity\_respects\_target\_distance\)\. Both bounds are necessary for the soundness of every subsequent FRI round\. Both initially stood assorryinlean/P3FriProofs/Proofs/FoldingCorrectness\.lean\. Both were closed in February 2026 by thealeph\-prover\[bot\]GitHub account, running Aleph against the Lean files\.

### 4\.1Aleph’s proof ofarity\_respects\_max\_bound

PR \#1 top3\-hax\-lean\-fri\-pipeline\[[2](https://arxiv.org/html/2605.30106#bib.bib35)\]was merged on 23 February 2026\. The PR description, generated by Aleph, identifies the following proof strategy: decompose into two reusable helper lemmas about the Hax\-extractedRustMmonad, peel the monadic binds ofcompute\_log\_arity\_for\_roundone by one, and reduce to the final “min with cap”if\.

The first helper inverts a successful monadic bind: ifx \>\>= f = ok r, then there exists someawithx = ok aandf a = ok r\.

1theoremRustM\_bind\_eq\_ok\{α\\alphaβ\\beta:Type\}\(x:RustMα\\alpha\)\(f:α\\alpha→\\toRustMβ\\beta\)\(r:β\\beta\):

2RustM\.bindxf=\.okr→\\to∃\\existsa,x=\.oka∧\\wedgefa=\.okr:=by

3casesxwith

4\|oka=\>

5introhx;refine⟨\\langlea,rfl,?\_⟩\\rangle

6simpa\[RustM\.bind\]usinghx

7\|faile=\>introhx;simp\[RustM\.bind\]athx

8\|div=\>introhx;simp\[RustM\.bind\]athx

The second helper derives a bound from the “min” if\-expression: if\(if a < b then ok a else ok b\) = ok r, thenr≤\\leqb\.

1theoremRustM\_ok\_ite\_decide\_lt\_le\_right\(abr:USize64\):

2\(ifdecide\(a<b\)then\(RustM\.oka:RustMUSize64\)elseRustM\.okb\)=

3RustM\.okr→\\tor≤\\leqb:=by

4introh

5by\_caseshlt:a<b

6⋅\\cdotsimp\[hlt\]ath;casesh

7havehnat:a\.toNat<b\.toNat:=bysimpausinghlt

8changea\.toNat≤\\leqb\.toNat

9exactNat\.le\_of\_lthnat

10⋅\\cdotsimp\[hlt\]ath;casesh;changeb\.toNat≤\\leqb\.toNat;exactle\_rfl

The main theorem unfoldscompute\_log\_arity\_for\_roundand usesRustM\_bind\_eq\_okto peel off the first checked subtraction\. It then case\-splits onnext\_input\_log\_height, peels the second bind in theSomebranch, and case\-splits on the inner<comparison\. Finally, it appliesRustM\_ok\_ite\_decide\_lt\_le\_rightto the “min\-with\-cap”if, bounding the result bymax\_log\_arity\. Aleph observes that the arithmetic preconditionh\_gtis unnecessary for this bound; this observation avoids any checked\-subtraction reasoning\.

### 4\.2Aleph’s proof ofarity\_respects\_target\_distance

PR \#3\[[3](https://arxiv.org/html/2605.30106#bib.bib36)\]was merged the following day, on 24 February 2026, with a symmetric strategy\. A single helper derives that\(if a < b then ok a else ok b\) = ok rimpliesr≤\\leqa:

1theoremRustM\_ok\_ite\_decide\_lt\_le\_left\(abr:USize64\):

2\(ifdecide\(a<b\)then\(RustM\.oka:RustMUSize64\)elseRustM\.okb\)=

3RustM\.okr→\\tor≤\\leqa:=by

4introh

5by\_caseshlt:a<b

6⋅\\cdotsimp\[hlt\]ath;casesh;changea\.toNat≤\\leqa\.toNat;exactle\_rfl

7⋅\\cdotsimp\[hlt\]ath;casesh

8changeb\.toNat≤\\leqa\.toNat

9applyNat\.le\_of\_not\_gt;simpausinghlt

The main theorem is more involved than in Section[4\.1](https://arxiv.org/html/2605.30106#S4.SS1)\. The conclusion

𝚛𝚎𝚜𝚞𝚕𝚝\.𝚝𝚘𝙽𝚊𝚝≤𝚕𝚘𝚐​\_​𝚌𝚞𝚛𝚛𝚎𝚗𝚝​\_​𝚑𝚎𝚒𝚐𝚑𝚝\.𝚝𝚘𝙽𝚊𝚝−𝚕𝚘𝚐​\_​𝚏𝚒𝚗𝚊𝚕​\_​𝚑𝚎𝚒𝚐𝚑𝚝\.𝚝𝚘𝙽𝚊𝚝\\mathtt\{result\.toNat\}\\leq\\mathtt\{log\\\_current\\\_height\.toNat\}\-\\mathtt\{log\\\_final\\\_height\.toNat\}involves checked subtraction onUSize64: at the Rust level the subtraction would have underflowed iflog\_final\_height≥\\geqlog\_current\_height, and the proof must discharge that case using the height\-inequality hypothesish\_gt\.

1theoremarity\_respects\_target\_distance

2\(log\_current\_heightlog\_final\_heightmax\_log\_arityresult:USize64\)

3\(h\_gt:log\_current\_height\.toNat\>log\_final\_height\.toNat\)

4\(h\_result:P3\_fri\_kernel\.compute\_log\_arity\_for\_round

5log\_current\_heightCore\_models\.Option\.Option\.None

6log\_final\_heightmax\_log\_arity=\.okresult\)

7:result\.toNat≤\\leqlog\_current\_height\.toNat\-log\_final\_height\.toNat:=by

8classical

9havehgt':log\_final\_height\.toNat<log\_current\_height\.toNat:=bysimpausingh\_gt

10havehnot:¬\\neg\(log\_current\_height\.toNat<log\_final\_height\.toNat\):=

11Nat\.not\_lt\_of\_ge\(Nat\.le\_of\_lthgt'\)

12unfoldP3\_fri\_kernel\.compute\_log\_arity\_for\_roundath\_result

13simp\[RustM\.bind,Core\_models\.Ops\.Arith\.Sub\.sub,instSubUSize64\_1,

14BitVec\.usubOverflow,hnot\]ath\_result

15havehle:result≤\\leqlog\_current\_height\-log\_final\_height:=by

16applyRustM\_ok\_ite\_decide\_lt\_le\_left

17\(a:=log\_current\_height\-log\_final\_height\)\(b:=max\_log\_arity\)\(r:=result\)

18by\_caseshlt:log\_current\_height\-log\_final\_height<max\_log\_arity<;\>

19simpa\[hlt\]usingh\_result

20havehleNat:result\.toNat≤\\leq\(log\_current\_height\-log\_final\_height\)\.toNat:=

21\(USize64\.le\_iff\_toNat\_le\)\.1hle

22havehsub:\(log\_current\_height\-log\_final\_height\)\.toNat=

23log\_current\_height\.toNat\-log\_final\_height\.toNat:=

24USize64\.toNat\_sub\_of\_le'\(Nat\.le\_of\_lthgt'\)

25simpa\[hsub\]usinghleNat

Both PRs are notable for how Aleph closed the theorems: by identifying and proving small reusable helper lemmas, then composing them in a structurally clean main proof\. The proof\-plan blueprints in the PR descriptions read like a proof engineer’s notes; for example, “decomposition into a key helper lemma and the main bound… the proof must useh\_gtto justify that the subtraction behaves like ordinaryℕ\\mathbb\{N\}subtraction ontoNat… the min/if structure is handled cleanly by aby\_casessplit andsimp\.”

## 5AI\-Driven Proof Automation: Empirical Notes

This section reports what we observed when running Aristotle and Aleph against the proof obligations that arose in our verification work\. We recognise the small size of our data set: two theorems that Aleph closed \(PR \#1 and PR \#3\), plus informal experiments on neighbouring lemmas during development\. Even so, we observed a consistent pattern throughout all our experiments\.

#### What AI provers handled well\.

Three categories of obligation closed reliably:

- •*Control\-flow and structural lemmas:*monad inversions, if\-conditional bounds, case\-splits on enums\. The two PRs of Section[4](https://arxiv.org/html/2605.30106#S4)fall here\. The reusable helper lemmas Aleph produced \(RustM\_bind\_eq\_ok,RustM\_ok\_ite\_decide\_lt\_le\_left/right\) are typical of this category\.
- •*Linear arithmetic with mild side conditions,*particularly whereomegaornlinarithcloses the goal once the right hypothesis is named\.
- •*simp\-closeable boilerplate*around extracted code: unfolding monadic bind, distributing over conditionals, normalising checked\-arithmetic guards\.

#### What required manual work\.

Three categories required either substantial manual proof or full hand\-construction:

- •*Domain\-specific algebraic identities*that require carefully selecting Mathlib4 lemmas\. A clear example is the equivalence between the Aeneas\-extractedfold\_stepand ArkLib’sfoldNth 2 fβ\\betaonℤ/p​ℤ\\mathbb\{Z\}/p\\mathbb\{Z\}polynomials\. The obligation is true, but no off\-the\-shelf Mathlib lemma closes it without human direction\.
- •*Loop invariants on Aeneas\-extracted recursive functions\.*We did not observe AI provers bypassing the inherent difficulty of finding the right invariant, so this remained a manual task in our work\.
- •*Obligations that require axiomatising an external interface,*where the choice of axioms is itself a design decision rather than a proof\-search problem\.

#### Implication for the workflow\.

In the work reported here, AI provers operated as a productivity multiplier on the obligations in the first category, but did not change the fundamental shape of the verification effort\. Specification design, invariant discovery, and the selection of mathematical abstractions remained the work of human proof engineers\. We expect this division to shift as AI provers mature, and Section[9](https://arxiv.org/html/2605.30106#S9)outlines two directions where we plan to push that line\.

## 6Case Studies

This section lists the cryptographic targets we verified under the zkEVM Verification Project\. All artefacts are public:

- •
- •
- •
- •
- •
- •
- •

Table 1:Verification targets under the zkEVM Verification Project\.#### Case study 1:fold\_step↔\\leftrightarrowArkLib\.

The arity\-2 FRI folding step takes evaluationsl​o=f​\(x\)lo=f\(x\)andh​i=f​\(−x\)hi=f\(\-x\)of a polynomialffover a prime fieldFpF\_\{p\}, together with a challengeβ\\betaand precomputed inversesx−1,2−1x^\{\-1\},2^\{\-1\}, and computes𝑓𝑜𝑙𝑑​\_​𝑠𝑡𝑒𝑝=\(l​o\+h​i\+β⋅\(l​o−h​i\)⋅x−1\)⋅2−1modp\\mathit\{fold\\\_step\}=\(lo\+hi\+\\beta\\cdot\(lo\-hi\)\\cdot x^\{\-1\}\)\\cdot 2^\{\-1\}\\bmod p\. This equals\(𝖿𝗈𝗅𝖽𝖭𝗍𝗁​2​f​β\)\.𝖾𝗏𝖺𝗅​\(x2\)\(\\mathsf\{foldNth\}\\,2\\,f\\,\\beta\)\.\\mathsf\{eval\}\(x^\{2\}\): one evaluation of the folded polynomial in ArkLib’s definition\. The Aeneas extraction unfolds the Rust into a sequence of 13 checked arithmetic operations onu64, each returningResult\. We proved, in Lean, that under explicit preconditions onpp\(p2≤264−1p^\{2\}\\leq 2^\{64\}\-1, all inputs strictly less thanpp\) no operation overflows, the final result is in\[0,p\)\[0,p\), and the algebraic expression matches the closed\-form above inℤ/p​ℤ\\mathbb\{Z\}/p\\mathbb\{Z\}\(verified by theringtactic\)\. This is the project’s tightest connection from Aeneas\-extracted production Rust to a formal cryptographic specification: the verifier checks not only that the arithmetic is overflow\-free, but that the Rust implementation computes exactly the function ArkLib defines\.

#### Case study 2: the running example revisited\.

This case study revisits the functioncompute\_log\_arity\_for\_roundand its correspondence to Aleph’s proofs\. It is the running example of Section[4](https://arxiv.org/html/2605.30106#S4)\. The Hax extraction produces a Lean 4 function over the HaxRustMmonad with two checked subtractions, anOptionmatch, and two if\-conditional “min” selections\. Six bounds\-style and boundary\-case theorems were stated\. Two were closed automatically by Aleph in PRs \#1 and \#3, each producing a small reusable helper lemma in addition to the main theorem\. The remaining four \(arity\_respects\_next\_input,folding\_respects\_final\_height,round\_consistency\_preserved, and one more\) currently remain atsorryin the public repository, awaiting either a follow\-up Aleph run or manual completion\.

#### Repositories and reproducibility\.

All code, specifications, and proofs in this paper are public:

- •
- •
- •Aleph PRs \#1\[[2](https://arxiv.org/html/2605.30106#bib.bib35)\]and \#3\[[3](https://arxiv.org/html/2605.30106#bib.bib36)\]\(running example\)\.

A complete list of per\-target repositories appears in the bullet list at the start of this section\.

## 7Engineering Challenges and Solutions

#### Lean 4 version drift\.

Aeneas, Hax, ArkLib, CompPoly, and Mathlib4 evolve on independent Lean 4 release tracks\. Early in the project we could not build a single Lake project that imported tools from more than one source, because each was pinned to a different Lean toolchain\. We raised the issue in the affected repositories; after coordination across the maintainer teams, the libraries were aligned on a common Lean 4 version \(4\.26\.0 for the Hax\-based work; 4\.28\.0 for the Aeneas\-based work\)\.

#### Aeneas/Hax extraction gaps\.

The supported subset of safe Rust that Aeneas and Hax can extract to pure Lean is finite\. We have identified the following gaps in practice:

- •A name collision \(BitVec\.toNat\_pow\) between Aeneas’s bit\-vector lemmas and Batteries / Mathlib4 prevented importing both libraries in a single Lean file\. We patched this upstream inAeneasVerif/aeneas\#832\.
- •Casts to wider integer types \(u128\) inside modular arithmetic require careful proof engineering:progressintroduces a side condition thatomegacannot close on its own and that needsnlinarith\.
- •Generic functions with trait bounds \(e\.g\.,F: Field \+ TwoAdicField\) cannot be extracted directly: Aeneas needs concrete monomorphised types\. We worked around this by writing a monomorphic model of the function in question \(Plonky3’sfold\_matrixrewritten as au64\-onlyfold\_step\); the model is semantically equivalent to the production code and extracts cleanly\.
- •External\-crate calls \(e\.g\.,byteorder,std::io::Read/Write\) are not extractable because Charon does not see the MIR of crates beyond the workspace\.
- •Rustwhileloops become recursive functions in Lean and require explicit termination measures\.

#### Three reliable workarounds\.

We converged on three strategies, applied in this order of preference:

1. 1\.*Fix it upstream\.*When a gap corresponds to a missing feature or lemma that we are able to contribute, we submit the fix to the upstream repository\. TheBitVec\.toNat\_powfix and several CompPoly contributions originated this way\.
2. 2\.*Extract a model\.*When the production Rust code uses patterns Aeneas cannot handle \(parallel iterators, deep generics, external\-crate calls\), we rewrite the mathematical core as a standalone, non\-generic Rust crate\. The model is semantically equivalent, extracts cleanly, and can be verified end\-to\-end\. This is the strategy that producedfold\_stepfrom Plonky3’sfold\_matrix\.
3. 3\.*Layered tools forunsafecode\.*The pipeline as described handles safe Rust\. For codebases withunsafeblocks, the verification story is layered: prove the safe core with Aeneas or Hax, and bring in complementary tools \(cargo\-anneal\[[29](https://arxiv.org/html/2605.30106#bib.bib31)\]\) for theunsafeparts\.

## 8Related Work

#### Rust formal verification\.

Aeneas and Hax are the two extraction\-based approaches we use directly\. The other major points in the verification space are Verus\[[16](https://arxiv.org/html/2605.30106#bib.bib24)\]\(ghost types and an SMT backend, tightly integrated with the Rust toolchain\), Prusti\[[4](https://arxiv.org/html/2605.30106#bib.bib25)\]\(specification annotations and the Viper verifier\), Kani\[[27](https://arxiv.org/html/2605.30106#bib.bib26)\]\(bounded model checking, complementary to formal proof\), and Creusot\[[10](https://arxiv.org/html/2605.30106#bib.bib27)\]\(Why3\-based deductive verification of annotated Rust\)\. These tools target different fragments of Rust and rely on different proof backends \(SMT solvers, Viper, Why3, model checking\)\. Our work instead focuses on connecting production Rust to Mathlib4\-level formal cryptographic specifications, and on integrating AI provers to close the resulting proof obligations\.

#### Foundational verified systems\.

seL4 and CompCert are landmark projects that demonstrate that complete formal verification of production\-quality software is achievable, but each represents many person\-years of effort in tightly coupled implementation and proof pairs in Isabelle/HOL and Rocq\. The pipeline described here requires substantially smaller per\-engagement effort, in exchange for verifying specific critical\-core components rather than whole systems\.

#### AI provers for Lean\.

LeanDojo\[[31](https://arxiv.org/html/2605.30106#bib.bib28)\]provides infrastructure for training and evaluating LLM\-based provers in Lean\. Lean Copilot\[[21](https://arxiv.org/html/2605.30106#bib.bib29)\]explores LLMs as interactive proof assistants inside the editor\. The AlphaProof and AlphaGeometry\[[30](https://arxiv.org/html/2605.30106#bib.bib30)\]effort from DeepMind demonstrated silver\-medal\-equivalent performance on IMO 2024 using reinforcement\-learning\-trained Lean provers\. Our work uses Aristotle\[[1](https://arxiv.org/html/2605.30106#bib.bib2)\]and Aleph\[[14](https://arxiv.org/html/2605.30106#bib.bib5)\]not as benchmarks on synthetic problems but as black\-box proof\-search engines on the proof obligations our extraction pipeline emits\. This is, to our knowledge, among the first publicly visible neurosymbolic deployments on production zkVM cryptographic code\.

#### Cryptographic specification libraries\.

ArkLib and CompPoly are the spec libraries this work targets\. Both are public and we contribute upstream to them\. The closest comparable project is HACL⋆for verified cryptographic implementations in F⋆, but its target language and specification style differ\.

## 9Conclusion and Future Work

We described an end\-to\-end neurosymbolic pipeline from production Rust to Lean 4 proofs, applied it to cryptographic primitives in Plonky3 and RISC Zero under the Ethereum Foundation zkEVM Verification Project, and gave an empirical account of where AI provers were and were not effective\. The two\-PR running example \(Aleph provingarity\_respects\_max\_boundandarity\_respects\_target\_distanceinp3\-hax\-lean\-fri\-pipeline\) shows that current AI provers can close non\-trivial structural lemmas about Hax\-extracted Rust monadic code, with proof plans that are themselves auditable\.

Two directions of follow\-up are immediate\. First, we plan to participate in the Beneficial AI Foundation’s Signal Shot programme\[[7](https://arxiv.org/html/2605.30106#bib.bib33)\], which targets end\-to\-end machine\-checked verification of the Signal messaging stack in Lean 4\. The Signal codebase is a natural next target for the same pipeline\. Second, we plan to integrate AI provers more tightly into the verification CI/CD loop\. Instead of invoking them per pull request, we would run them automatically on every freshly introducedsorryand let human reviewers see which obligations are now closed before they look at the code\.

#### Acknowledgements\.

This work was funded by the Ethereum Foundation under the zkEVM Verification Project\. We are grateful to Alexander Hicks and Derek Sorensen for initiating and guiding this engagement, providing feedback on specifications and proofs, and facilitating the collaboration across teams\. We also thank the maintainers of Aeneas, Charon, Hax, Mathlib4, ArkLib, CompPoly, Aristotle, and Aleph for their open\-source work and for cross\-repository coordination on Lean toolchain alignment\.

## References

- \[1\]T\. Achim, A\. Best, A\. Bietti, K\. Der,et al\.\(2025\)Aristotle: IMO\-level automated theorem proving\.External Links:2510\.01346,[Link](https://arxiv.org/abs/2510.01346)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p4.1),[§2\.4](https://arxiv.org/html/2605.30106#S2.SS4.p1.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px3.p1.1)\.
- \[2\]Aleph Prover Bot\(2026\)Proof forarity\_respects\_max\_bound, PR \#1\.Note:[https://github\.com/runtimeverification/p3\-hax\-lean\-fri\-pipeline/pull/1](https://github.com/runtimeverification/p3-hax-lean-fri-pipeline/pull/1)Cited by:[§4\.1](https://arxiv.org/html/2605.30106#S4.SS1.p1.1),[3rd item](https://arxiv.org/html/2605.30106#S6.I2.i3.p1.1)\.
- \[3\]Aleph Prover Bot\(2026\)Proof forarity\_respects\_target\_distance, PR \#3\.Note:[https://github\.com/runtimeverification/p3\-hax\-lean\-fri\-pipeline/pull/3](https://github.com/runtimeverification/p3-hax-lean-fri-pipeline/pull/3)Cited by:[§4\.2](https://arxiv.org/html/2605.30106#S4.SS2.p1.1),[3rd item](https://arxiv.org/html/2605.30106#S6.I2.i3.p1.1)\.
- \[4\]V\. Astrauskas, A\. Bílý, J\. Fiala, Z\. Grannan, C\. Matheja, P\. Müller, F\. Poli, and A\. J\. Summers\(2022\)The Prusti Project: Formal verification for Rust\.InNASA Formal Methods \(NFM\),pp\. 88–108\.Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px1.p1.1)\.
- \[5\]C\. Barrett, S\. Chaudhuri, F\. Montesi, J\. Grundy, P\. Kohli, L\. de Moura, A\. Rademaker, and S\. Yingchareonthawornchai\(2026\)CSLib: The Lean Computer Science Library\.External Links:2602\.04846,[Link](https://arxiv.org/abs/2602.04846)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p5.1)\.
- \[6\]E\. Ben\-Sasson, I\. Bentov, Y\. Horesh, and M\. Riabzev\(2018\)Scalable, transparent, and post\-quantum secure computational integrity\.Note:IACR Cryptology ePrint Archive, 2018/046External Links:[Link](https://eprint.iacr.org/2018/046)Cited by:[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p1.1),[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p2.1),[§4](https://arxiv.org/html/2605.30106#S4.p1.1)\.
- \[7\]Beneficial AI Foundation\(2026\)Signal Shot: end\-to\-end formal verification of the Signal protocol\.Note:[https://www\.beneficialaifoundation\.org/blog/signal\-shot](https://www.beneficialaifoundation.org/blog/signal-shot)Cited by:[§9](https://arxiv.org/html/2605.30106#S9.p2.1)\.
- \[8\]A\. Chiesa, Y\. Hu, M\. Maller, P\. Mishra, N\. Vesely, and N\. P\. Ward\(2019\)Marlin: Preprocessing zkSNARKs with universal and updatable SRS\.Note:IACR Cryptology ePrint Archive, 2019/1047Cited by:[§2\.3](https://arxiv.org/html/2605.30106#S2.SS3.p2.1)\.
- \[9\]Cryspen\(2024\)Hax: Verification\-friendly Rust subset\.Note:[https://github\.com/cryspen/hax](https://github.com/cryspen/hax)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p3.1),[§2\.2](https://arxiv.org/html/2605.30106#S2.SS2.p1.2)\.
- \[10\]X\. Denis, J\. Jourdan, and C\. Marché\(2022\)Creusot: A foundry for the deductive verification of Rust programs\.InInternational Conference on Formal Engineering Methods \(ICFEM\),Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px1.p1.1)\.
- \[11\]Ethereum Foundation\(2025\)zkEVM Verification Project\.Note:[https://github\.com/Verified\-zkEVM/](https://github.com/Verified-zkEVM/)Cited by:[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p3.1)\.
- \[12\]Formal Land\(2024\)Rocq\-of\-rust\.Note:[https://github\.com/formal\-land/rocq\-of\-rust](https://github.com/formal-land/rocq-of-rust)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p3.1)\.
- \[13\]S\. Ho and J\. Protzenko\(2022\)Aeneas: Rust verification by functional translation\.Proceedings of the ACM on Programming Languages6\(ICFP\),pp\. 711–741\.External Links:[Document](https://dx.doi.org/10.1145/3547647)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p3.1),[§2\.1](https://arxiv.org/html/2605.30106#S2.SS1.p1.1),[§2\.1](https://arxiv.org/html/2605.30106#S2.SS1.p2.1)\.
- \[14\]V\. Isenbaev and B\. Hanin\(2026\)Logical Intelligence’s Aleph Solves PutnamBench\.Note:Logical Intelligence BlogExternal Links:[Link](https://logicalintelligence.com/blog/aleph-solves-putnambench)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p4.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px3.p1.1)\.
- \[15\]G\. Klein, K\. Elphinstone, G\. Heiser, J\. Andronick, D\. Cock, P\. Derrin, D\. Elkaduwe, K\. Engelhardt, R\. Kolanski, M\. Norrish, T\. Sewell, H\. Tuch, and S\. Winwood\(2009\)seL4: Formal verification of an OS kernel\.InProceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles \(SOSP\),pp\. 207–220\.External Links:[Document](https://dx.doi.org/10.1145/1629575.1629596)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1)\.
- \[16\]A\. Lattuada, T\. Hance, C\. Cho, M\. Brun, I\. Subasinghe, Y\. Zhou, J\. Howell, B\. Parno, and C\. Hawblitzel\(2023\)Verus: Verifying Rust programs using linear ghost types\.InProceedings of the ACM on Programming Languages, OOPSLA,Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px1.p1.1)\.
- \[17\]X\. Leroy\(2009\)Formal verification of a realistic compiler\.Communications of the ACM52\(7\),pp\. 107–115\.Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1)\.
- \[18\]Logical Intelligence\(2025\)Aleph Prover\.Note:[https://logicalintelligence\.com/aleph\-prover\.html](https://logicalintelligence.com/aleph-prover.html)Accessed 2026\-05\-22Cited by:[§2\.4](https://arxiv.org/html/2605.30106#S2.SS4.p1.1)\.
- \[19\]Polygon Zero\(2024\)Plonky3: High\-performance polynomial commitment and proof system\.Note:[https://github\.com/Plonky3/Plonky3](https://github.com/Plonky3/Plonky3)Cited by:[2nd item](https://arxiv.org/html/2605.30106#S1.I1.i2.p1.1),[§1](https://arxiv.org/html/2605.30106#S1.p6.1),[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p1.1),[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p2.1)\.
- \[20\]RISC Zero, Inc\.\(2024\)RISC Zero: zero\-knowledge virtual machine for general Rust programs\.Note:[https://github\.com/risc0/risc0](https://github.com/risc0/risc0)Cited by:[2nd item](https://arxiv.org/html/2605.30106#S1.I1.i2.p1.1),[§1](https://arxiv.org/html/2605.30106#S1.p6.1),[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p1.1)\.
- \[21\]P\. Song, K\. Yang, and A\. Anandkumar\(2024\)Towards large language models as copilots for theorem proving in Lean\.External Links:2404\.12534Cited by:[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px3.p1.1)\.
- \[22\]Succinct Labs\(2024\)SP1: zkVM\.Note:[https://github\.com/succinctlabs/sp1](https://github.com/succinctlabs/sp1)Cited by:[§2\.5](https://arxiv.org/html/2605.30106#S2.SS5.p1.1)\.
- \[23\]Symbolic Software\(2026\)The Verification Facade: Structural Gaps in Cryspen’s Hax Pipeline\.Note:Symbolic Software BlogExternal Links:[Link](https://symbolic.software/blog/2026-04-07-cryspen-hax/)Cited by:[§2\.2](https://arxiv.org/html/2605.30106#S2.SS2.p2.1)\.
- \[24\]The Aeneas Project\(2024\)Charon: Rust to LLBC translator\.Note:[https://github\.com/AeneasVerif/charon](https://github.com/AeneasVerif/charon)Cited by:[§2\.1](https://arxiv.org/html/2605.30106#S2.SS1.p1.1)\.
- \[25\]The ArkLib Team\(2025\)ArkLib: Formal verification of cryptographic protocols in Lean 4\.Note:[https://github\.com/Verified\-zkEVM/ArkLib](https://github.com/Verified-zkEVM/ArkLib)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p5.1),[§2\.3](https://arxiv.org/html/2605.30106#S2.SS3.p2.1)\.
- \[26\]The CompPoly Team\(2025\)CompPoly: Computational polynomial theory in Lean 4\.Note:[https://github\.com/Verified\-zkEVM/CompPoly](https://github.com/Verified-zkEVM/CompPoly)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p5.1),[§2\.3](https://arxiv.org/html/2605.30106#S2.SS3.p3.1)\.
- \[27\]The Kani Team\(2024\)Kani Rust Verifier\.Note:[https://github\.com/model\-checking/kani](https://github.com/model-checking/kani)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p2.1),[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px1.p1.1)\.
- \[28\]The mathlib Community\(2024\)Mathlib4\.Note:[https://github\.com/leanprover\-community/mathlib4](https://github.com/leanprover-community/mathlib4)Cited by:[§1](https://arxiv.org/html/2605.30106#S1.p5.1)\.
- \[29\]The zerocopy Authors\(2026\)cargo\-anneal: Specifications and soundness proofs for unsafe Rust\.Note:[https://crates\.io/crates/cargo\-anneal](https://crates.io/crates/cargo-anneal)Cited by:[item 3](https://arxiv.org/html/2605.30106#S7.I2.i3.p1.1)\.
- \[30\]T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong\(2024\)Solving olympiad geometry without human demonstrations\.Note:DeepMind blog and Nature publicationExternal Links:[Link](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)Cited by:[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px3.p1.1)\.
- \[31\]K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: Theorem proving with retrieval\-augmented language models\.InNeurIPS,Cited by:[§8](https://arxiv.org/html/2605.30106#S8.SS0.SSS0.Px3.p1.1)\.