Source-linked AI summary
Solving VeriContest with a Lean-Backed Rust Verifier
Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi
TL;DR
Proof generation is the bottleneck for frontier models on VeriContest, a benchmark of Rust programs and Verus specifications. Rust-Prover translates the specifications and code into Lean theorems and has agents prove them for kernel checking. It proves all benchmark theorems, with the conclusion supported by the reported clean-check and validation results.
Problem
VeriContest authors identify proof generation as the bottleneck for frontier models given Rust code and specifications.
Source: §2 · p. 2Method
Rust-Prover restates specifications, translates Rust code and specifications into Lean theorems, and has agents prove them for Lean’s kernel to check.
Source: §3.2 · p. 4, §3.4 · p. 5Results
All 1325 theorems across 1007 problems were proved and re-checked in a clean clone, with no axioms beyond Lean’s three standard ones.
Source: §1 · p. 1Takeaways & Limitations
Every VeriContest theorem now has a Lean proof checked by Lean’s kernel, with no axioms beyond the standard three.
Source: §5 · p. 10The ten-theorem model-effort sample is small and contains few hard theorems, so its figures are indicative.
Source: §4.4 · p. 7
Abstract
from arXiv · showhide
VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specification and the code, the best model produces an accepted Verus proof for 13.95% of the problems on the first attempt. We report on solving the same proof-generation task with Rust-Prover, a verifier for Rust backed by Lean 4. The Verus specification and the Rust code are restated and translated into Lean, each specification becomes a theorem, and agents prove the theorems with Lean's kernel as the final check. All 1325 theorems of all 1007 problems were proved. 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5, at a median of 3.2 minutes and $1.17 per proof, and 70% of them on the first iteration. The restated specifications were checked against the benchmark's test suites, and reviewed where no suite applies. None was wrong or weakened. The translated Lean programs were run on 21,413 of the benchmark's test cases and produced the same output as the Rust programs on every one. Across four Claude and four GPT models at five reasoning-effort settings, every current frontier model proves nearly all of a ten-theorem sample at every setting, and more effort raises the cost without raising the number of proofs. The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems. We also rerun the benchmark's own Verus protocol with Claude Opus 5.5 on the 50 problems with the longest reference proofs. Opus 5.5 alone fails to prove one of them.
1 Introduction
Rust-Prover applies Lean 4 verification to Rust code, motivated by Rust’s role in blockchain infrastructure. On VeriContest, it proves every theorem while validating the restated specifications and studying model performance.
1 Introduction
- Rust-Prover targets Rust verification, relevant because much blockchain infrastructure and its surrounding services are written in Rust.The verifier is backed by Lean 4.Source: §1 · p. 1
- The paper applies Rust-Prover to VeriContest’s proof-generation task, replacing Verus proofs with Lean proofs for benchmark problems.The benchmark contains about a thousand Rust problems with expert-reviewed Verus specifications and proofs.Source: §1 · p. 1
- All 1325 theorems across 1007 problems were proved and re-checked in a clean clone, using no axioms beyond Lean’s three standard ones.The restated specifications were checked against test suites or reviewed where suites did not apply; translated programs were validated on 19,555 executed cases.Source: §1 · pp. 1–2
- The evaluation studies five Claude and four GPT models across five reasoning-effort settings, plus cheaper models on hard theorems and the full benchmark.Agents prove Lean theorems that state the specifications, and Lean’s kernel checks the proofs.Source: §1 · pp. 1–2
2 VeriContest
VeriContest evaluates verifiable Rust code generation across 1007 problems. Its authors identify proof generation as the bottleneck for frontier models.
2 VeriContest
- VeriContest’s September 2026 benchmark state contains 1007 problems, each with a Rust solution, Verus specification, proof, and test suites.The main set has 946 problems; 61 extended problems are excluded from the paper’s evaluation because their outputs require problem-specific judges and they lack test suites.Source: §2 · p. 2
- ProofGen asks a model to make Verus accept supplied code and specifications using proof annotations, without changing either.The benchmark also defines SpecGen, CodeGen, and End2End tasks.Source: §2 · p. 2
- Proof generation is the bottleneck among VeriContest’s evaluated tasks for frontier models.The authors report that GPT-5.5 had the highest scores, as shown in Table 1.Source: §2 · p. 2, Table 1 · p. 2
3 Rust-Prover on VeriContest
Rust-Prover restates VeriContest specifications, translates Rust programs into Lean, turns specifications into theorems, and uses automation and agents to prove them for kernel checking.
3 Rust-Prover on VeriContest
- For ProofGen, Rust-Prover receives the Verus specification, Rust code, and English description, then must produce a Lean proof without seeing benchmark proof annotations.The code and specification are not altered by the agents.Source: §3 · p. 3
3.1 Step 1. Restate the specification
- Specifications are restated in Rust-Prover’s format using a transpiler where possible and agents for the remainder, following a porting guide.The example specification expresses the required signed-integer reversal behavior, returning 0 when the reversed value does not fit.Source: §3.1 · p. 3
3.2 Step 2. Translate the crate into Lean
- Forks of Charon and Aeneas translate the crate into Lean; Aeneas represents mutable references as input and output values, loops recursively, and arithmetic as Results.The authors state that the resulting Lean program has the same meaning as the crate.Source: §3.2 · p. 4
3.3 Step 3. Turn the spec into a theorem
- The Lean command #derive_spec turns each specification into a theorem whose successful result entails that its postcondition held.The 1007 problems yield 1325 theorems because some postconditions are stated in separate specification functions.Source: §3.3 · p. 4
3.4 Step 4. Prove the theorems
- A fixed tactic sequence runs first, then agents prove remaining goals under iteration and time limits; every accepted proof is checked against an unchanged theorem statement and Lean’s axiom rules.For Reverse Integer, Opus 5.5 independently found an invariant essentially matching the benchmark’s unseen Verus proof, in three checks and about two minutes.Source: §3.4 · pp. 4–5
4 Results
Rust-Prover translated VeriContest specifications and programs into Lean theorems, which agents proved and Lean’s kernel checked. All 1,325 theorems were proved, alongside additional tests of translation fidelity and model comparisons.
4.1 Specification translation
- Of 1,007 translated specifications, 658 were validated against benchmark test suites, while the other 349 could not be checked by suites and were agent-reviewed against the Verus original under a written protocol.Source: §4.1 · p. 5
4.2 Code translation
- All 1,007 programs translated to Lean; 19,555 executed test cases agreed with Rust, while nine problems could not be run.The 19,555 cases came from 105 of the 114 problems the harness could try.Source: §4.2 · p. 6
4.3 Proof generation
- All 1,325 theorems were proved; 944 of 1,325 passed the first check, and the full run cost $1,792.A typical proof took about three minutes; the hardest difficulty class cost three times as much as the easiest.Source: §4.3 · p. 6
- The hardest difficulty class took about 3.5 times as long and cost three times as much as the easiest, with no more proof iterations.The difficulty analysis covered 1,266 of the 1,325 proofs.Source: §4.3 · p. 6, Table 3 · p. 6
4.4 Models and reasoning effort
- Fable, Opus, GPT-6 Astra, and GPT-6.1 Sol proved all ten sampled theorems at every effort setting; more effort bought additional proofs only for Luna and Haiku 5.5.The ten-theorem sample was small, and the authors treat these figures as indications.Source: §4.4 · p. 7
- Sonnet 5.5 at low effort proved all 50 theorems the main run spent the most time on, 48 at the first iteration.The authors note that the two runs differ in more than the model, so this is not a controlled comparison.Source: §4.4 · p. 8
- A Luna-first run proved all 1,325 theorems for a recorded $643, with Opus rescuing 179 that Luna failed; missing Luna session records make the true cost higher.The recorded cost was $0.48 per proof, and the run did not include the main run’s clean-clone re-check.Source: §4.4 · p. 8
4.5 Comparison with the VeriContest paper
- Across 50 problems, Opus 5.5’s Verus protocol proved 49, while Rust-Prover proved all 65 theorems mapped to 47 problems; their proof setups differ in re-checkability.Rust-Prover proved 50 of 65 at the first official check; Opus 5.5 succeeded on 36% of a single API call, and these rates are not comparable.Source: §4.5 · pp. 9–10
5 Conclusion
The paper reports Lean proofs for every VeriContest theorem, with Lean’s kernel checking each proof. It identifies transfer to customer specifications, cheap-model limits, and possible benchmark-answer exposure as open questions.
5 Conclusion
- Every theorem in VeriContest now has a Lean proof, checked by Lean’s kernel with no axioms beyond the standard three.Agents wrote proofs at a median of three minutes and about a dollar each.Source: §5 · p. 10
- It remains unknown how well these results transfer to customer crates, where specifications are written from scratch rather than restated from a benchmark.Source: §5 · p. 10
- The limit of cheap models remains unknown: Sonnet 5.5 at low effort proved the hardest 50 theorems, and a Luna-first run proved the whole benchmark at a third of the recorded cost.Source: §5 · p. 10
- Because VeriContest’s Verus proofs are public, the authors cannot rule out answer exposure for the Verus rerun; no Lean proofs existed before this study.Source: §5 · p. 10
A The 27 specializations
Table 8 covers 27 problems whose code or specification helper was re-encoded.
A The 27 specializations
- Table 8 lists 27 problems whose code or specification helper was re-encoded.Source: Table 8 · p. 11