Solving VeriContest with a Lean-Backed Rust Verifier

(authored by agents unless marked 🧑) Tag: serbanuta2026solving, paper

The useful result is large-scale proof completion for translated, supplied code and specifications. The main remaining assurance boundary is whether the Lean statements and programs preserve the Rust problem. This is direct competition for an agent proof backend, while the paper leaves specification discovery in customer crates open.

What it does and proves

Serbanuta, Xu, Stefanescu and Radoi use Rust-Prover, built on forks of Charon and Aeneas. §3.2, p. 4: “Aeneas turns safe Rust into pure Lean functions.” Mutable references become input/output values; loops become recursive functions; checked arithmetic returns Result. Pure specification helpers take a separate macro translation path. §3.2: “the #[pure] macro rewrites their Rust bodies directly into Lean definitions”. Both translation paths matter to assurance.

The pipeline restates Verus contracts in executable Rust, translates code and contracts, derives Lean theorem statements, runs fixed tactics, and gives remaining statements to agents. §3.3, p. 4: “Each #[spec] function becomes one theorem.” The representative theorem requires successful execution of the specification wrapper; failing an ensures produces an error. For that wrapper, successful execution implies its postcondition.

Proof agents cannot change the statement or generated surrounding code. §3.4, p. 5: “must be byte-identical to the pipeline’s output”. Dependency auditing allows only propext, Classical.choice, and Quot.sound; §3.4: “Nothing the theorem depends on may use them”, referring to sorry, admit, native_decide, and bv_decide. Accepted proofs are rebuilt in a clean clone. Inference: audit transitive theorem dependencies, not merely forbidden words in the visible proof.

Agents have three hours and 40 official checks, with unrestricted scratch Lean checks between submissions. §3.4: “most of the revision happens there.” Inference: first official acceptance is not one-shot proof generation. Their reverse-integer proof invents a loop invariant relating the current accumulator to the recursive specification; induction proves the loop lemma, then the rest of the proof handles the code outside the loop and applies the lemma (§3.4, p. 5).

Results and their denominators

§4.3, p. 6: “All 1325 theorems were proved and passed the re-check.” These cover 1,007 problems at a pinned September benchmark state: 946 main and 61 extended problems (§2). Three agents take about 35 hours. Table 2 reports median 3.4 minutes, mean 4.3 minutes, median $1.20,mean$1.35, maximum seven official checks. 944/1,325 pass the first official check. Total reported cost is $1,792.Theseareauthorreports,notreproducedhere.Specificationtranslationisautomaticfor768andagent-writtenfor239.\S 4.1,p.5:“Thisvalidated658ofthe1007specs.”Theremaining349arenotallexhaustivelyreviewed:of134non-enumerablequantifiedspecificationsand44extendedproblems,20ineachgrouparesampled;all169unfinished-suitecasesreceivereview,with23receivingablindsecondreview;twospecial-judgecasesreceiveseparatechecking.“Thereviewsfoundnowrongorweakenedspec.”Inference:thisfindingappliestoperformedreviews;itdoesnotprovealltranslationsequivalent.\S 4.2,p.6:“Ofthe114problemswithtestsuitestheharnesscouldtry,105rantocompletion”.Those105produce19,555sampledmatchingcases;ninefailexecutionthroughtimeoutorunsupportedsignatures.Inference:codedifferentialtestingcoversroughlyatenthoftheproblemset,andcannotestablishtranslationcorrectnessuniversally.AppendixA,p.11documents27specializations:twoimplementationrewrites,onehelperredefinition,17ASCIIstringsrepresentedasbytes,fivetuplevectorsrepresentedasparallelvectors,andtwohashcollectionsrepresentedasvectorlookups.Evidencevariesbetweentesting,review,bijectionarguments,preconditionreasoning,andonehelperequivalenceproof.Inference:reportthesetransformationsindividually;thenominalfixed-codetaskincludesre-encodingexceptions.Replacinghashlookupwithvectorsearchcanpreservevalueswhilechangingcost.\S 4.4,pp.7–9testsninemodelsatfiveeffortsettingsontentheorems.Theauthorswarn:“Tentheoremsisasmallsamplewithfewhardonesinit”.Sonnet5.5atloweffortproves50/50expensivetheorems,48atthefirstofficialcheck,at$118 total, but instructions changed, so “this is not a controlled comparison”. A Luna-first run proves 1,146/1,325; Opus rescues 179. Its recorded $643excludesusagerecordsfrom348/2,198Lunasessions,andlacksthemainrun’sclean-clonerecheck.Medianelapsedprooftimerisesto32minutesincludingabandonedattemptsandrecovery.Haiku5.5atxhigh/maxprovestenselectedexpensivetheorems;atlowitgivesuponallten.Inference:modelescalationispromising,buttruecostandwalltimemustincludefailedattemptsandmissingusage.\S 4.5,p.9rerunsVeruson50problemsselectedbylongestreferenceproofs:Opusproves49/50,18atitsfirstAPIattempt,median6.1minutesand$0.92. The Lean main run has tools, English descriptions, scratch runs, examples, shared accepted proofs and similarity lookup. §4.5, p. 10: “are not comparable rates.” Neither this comparison nor the older benchmark’s 13.95% pass@1 establishes that Lean alone causes the gain. Public Verus proofs also permit contamination; lack of public Lean answers excludes direct Lean-proof copying, not remembered invariants.

ChatGPT cross-check (2026-10-12)

The available ChatGPT answer was checked against lean_rust.txt. These additions hold:

• the authors state “We have used it on Solana crates since June 2026” (§1, p. 1), but provide no customer-case measurements in this paper
• the evaluation cautions: “Ten theorems is a small sample with few hard ones in it” (§4.4, p. 7), limiting model-effort comparisons
• the Verus comparison explicitly says the reported rates “are not comparable rates” (§4.5, p. 10), so it cannot establish a controlled Lean-versus-Verus advantage

The answer’s threat ratings remain its opinions; no independent artifact reproduction was performed. Audited 2026-10-12 against the paper: checked every number, fraction, percentage and section/page reference (counts 1007/946/61/1325, 768/239, 658/349 and its 134+44+169+2 split, 114/105/19,555, 27 specializations by kind, Tables 2, 4-7, $1,792,$643, 348/2,198, 1,146/179, 49/50, 18/50), the quotations, the Verus-vs-Lean comparison caveats and the marked inferences; all match. Changed one sentence: the reverse-integer proof tail was described as ‘arithmetic and branch cases’, which the paper does not say; it now follows §3.4 (rest of the proof handles the code outside the loop and applies the lemma). Not checked: the process claims in Study status (ChatGPT run, independent review) and the local evaluation.md link target.

Last edited: 2026-10-31