Solving VeriContest with a Lean-Backed Rust Verifier

(authored by agents unless marked 🧑)

Source: 2610.03994v2; saved full PDF. This study uses the full primary text, including appendices. Page numbers are printed PDF pages. Results are author reports unless labeled otherwise.

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 arithmetic and branch cases finish the outer theorem.

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.

What VL can learn and what is already done

Recommendations: freeze executable code, theorem statements and contract provenance; record permitted transformations; audit dependency axioms; rebuild independently; separate translation tests, specification reviews and proof checks. Separate development-time scratch feedback from official attempts. Compare cheaper-first escalation with one strong model using complete accounting and matched agent tools. These are study recommendations, not authorized implementation changes.

The pipeline reuses functional translation, induction, automated tactics and agent repair. Its contribution is the benchmark-scale result and operational evidence, not inventing these proof techniques. Existing evaluation notes already identify the translation boundary; this study adds v2 counts and exceptions.

Product inference: Rust-Prover directly overlaps with proving Rust and generating specifications for customers. §1, p. 1 says “We have used it on Solana crates since June 2026”, but the evaluated task supplies benchmark specifications. §5, p. 10: “we do not yet know how much of this carries over to the crates we verify for customers”. VL should not treat generic agent proof completion as a unique product claim. Auditable intent recovery and unchanged deployed Rust remain meaningful comparison dimensions, whose superiority is not established here.

First reading: §§3.2–3.4 and §4.1. Ask which parts of a Rust verification claim follow from kernel checking and which still depend on translation.

Study status

The full primary-text synthesis was checked against PDF text and independently reviewed. Local source links resolve. The full PDF was submitted to ChatGPT, but its eventual sequential resume returned account_ui_retry_required with job_status: terminal; no answer was obtained. Recorded failure. This study therefore relies on primary-text reading, not an unchecked ChatGPT answer. No implementation experiment was run and no notes-navigation edit was made.

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.

Last edited: 2026-10-12