Paper deep dive
Solving VeriContest with a Lean-Backed Rust Verifier
Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 10/6/2026, 10:32:24 AM
Summary
This paper introduces Rust-Prover, a verification framework for Rust backed by Lean 4, applied to the VeriContest benchmark. The authors translated 1007 Rust competitive programming problems and their Verus specifications into Lean, generating 1325 theorems. Using AI agents (primarily Claude Opus 5.5 and Sonnet 5.5), all theorems were proved, with 70% accepted on the first iteration. The study highlights that Lean's kernel provides a re-checkable proof standard, contrasting with Verus solver verdicts, and demonstrates that frontier models can solve proof generation tasks efficiently when provided with iterative feedback from a formal verifier.
Entities (11)
Relation Signals (9)
Rust-Prover → appliedto → VeriContest
confidence 98% · This paper reports on running Rust-Prover against VeriContest
Rust-Prover → uses → Lean 4
confidence 98% · Rust-Prover, a verifier for Rust backed by Lean 4.
Claude Opus 5.5 → proved → VeriContest
confidence 95% · 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5
Rust-Prover → translates → Rust
confidence 95% · The crate, spec included, is translated into Lean by our forks of Charon and Aeneas.
GPT-5.5 → achievedhighscoreon → VeriContest
confidence 90% · The highest scores were GPT-5.5’s, shown in Table 1.
Claude Sonnet 5.5 → proved → VeriContest
confidence 90% · The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems.
Rust-Prover → translates → Verus
confidence 90% · The Verus specification is first restated as a Rust-Prover spec.
Rust-Prover → usedon → Solana
confidence 85% · We have used it on Solana and Sui crates since spring 2026.
Rust-Prover → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2610.03994v1
- Canonical: https://arxiv.org/abs/2610.03994v1
Trouble viewing inline? Open PDF directly →
Full Text
25,372 characters extracted from source content.
Expand or collapse full text
Solving VeriContest with a Lean-Backed Rust Verifier Traian Serbanuta Jun Xu Andrei Stefanescu Cosmin Radoi Asymptotic October 2026 Abstract 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 Much of the infrastructure that runs blockchains and the services around them is written in Rust. We have built Rust-Prover, a verifier for Rust backed by Lean 4 [1], to verify such code as it ships. Rust-Prover works in three steps. Agents write a specification from a description of the intended behaviour. The code and the specification are translated into Lean, where each specification becomes a theorem. Automated tactics and agents prove the theorems, and Lean’s kernel checks the proofs. We have used it on Solana and Sui crates since spring 2026. This paper reports on running Rust-Prover against VeriContest [5], a public benchmark of about a thousand competitive-programming problems in Rust with expert-reviewed Verus [4] specifications and proofs. We take the benchmark’s proof-generation task, in which a model receives the specification and the code and must produce a proof, and solve it with Lean proofs instead of Verus proofs. Our contributions are the following. • All 1325 theorems of all 1007 problems were proved and re-checked in a clean clone, with no axioms beyond Lean’s three standard ones (Section 4.3). • The restated specifications were validated against the benchmark’s test suites, and by review where no suite applies (Section 4.1). The translated programs were validated on 21,413 of the benchmark’s test cases (Section 4.2). • A study of four Claude and four GPT models at five reasoning-effort settings, and of the cheapest Claude setting on the 50 hardest theorems (Section 4.4). 2 VeriContest VeriContest is a benchmark for verifiable code generation in Rust, published in May 2026. Its main set has 946 problems, 690 from LeetCode and 256 from Codeforces. Each problem comes with the original natural-language description, a Verus specification reviewed by experts, a Rust solution accepted by the online judge, a Verus proof that the solution meets the specification, and two test suites, one of correct cases and one of mutated cases that a correct specification must reject. The repository also ships 61 extended problems, verified the same way but left out of the paper’s evaluation because their outputs need a problem-specific judge. The extended problems have no test suites. In total there are 1007 problems. The benchmark defines four tasks for a model. • SpecGen. Read the description and write the specification. Graded mainly by running the specification against both test suites. • CodeGen. Write the program from the description, the specification or both. Graded on the tests. • ProofGen. Given the specification and the code, make Verus accept them. That means adding proof annotations to the code, such as loop invariants, assertions, termination measures and calls to helper lemmas, until the solver can check the specification. The specification and the code may not be changed. • End2End. Do all three from the description alone. The authors evaluated ten frontier models. The highest scores were GPT-5.5’s, shown in Table 1. Code generation is almost solved. Proof generation is the bottleneck. Task pass@1 CodeGen (description to code) 92.18 % SpecGen (description to spec) 48.31 % ProofGen (spec + code to Verus proof) 13.95 % End2End 5.29 % Table 1: GPT-5.5 on VeriContest, as reported by the benchmark’s authors. pass@1 is the share of problems solved on the first attempt. The model is asked once and that one output is checked. 3 Rust-Prover on VeriContest We challenge Rust-Prover with ProofGen. For each problem it gets the same two inputs the task gives a model, the Verus specification and the Rust code, and has to produce a Lean proof that the code meets the specification. The benchmark’s own proof annotations, such as loop invariants, are not translated, and the agents never see them. 3.1 Step 1. Restate the specification The Verus specification is first restated as a Rust-Prover spec. A transpiler does this where it can, and an agent writes the spec for the rest, following a porting guide. Take problem 7, Reverse Integer, as an example. The benchmark’s code is a simple accumulator loop (abridged): ⬇ pub fn reverse(x: i32) -> i32 if x == i32::MIN return 0; let neg = x < 0; let mut cur: i32 = if neg -x else x ; let mut res: i32 = 0; while cur != 0 // omitted: res = res * 10 + cur % 10 with checked arithmetic, return 0 on overflow cur = cur / 10; if neg -res else res The benchmark’s specification requires that the function return the digits of a signed 32-bit integer in reverse, and 0 exactly when the reversed number does not fit. Restated for Rust-Prover, it reads as follows. ⬇ #[pure] pub fn reverse_spec_helper(x: Nat, acc: Nat) -> Nat decreases(x); if x == 0.to_nat() acc else let new_acc = acc * 10.to_nat() + x % 10.to_nat(); if new_acc > i32::MAX.to_int().to_nat() 0.to_nat() else reverse_spec_helper(x / 10.to_nat(), new_acc) #[spec] pub fn reverse_vc_spec(x: i32) -> i32 requires(i32::MIN <= x); requires(x <= i32::MAX); let out = reverse(x); ensures(out.to_int() == reverse_spec(x.to_int())); out The restated specification is plain Rust, in the style of our Sui Prover. A spec is a function marked #[spec] that calls the code and states its contract with requires and ensures. reverse_spec_helper defines the expected result over unbounded naturals, including the rule that a result too large for an i32 is 0, and reverse_spec, not shown, handles the sign and calls it. The #[pure] attribute marks them as pure, and decreases says the recursion terminates. 3.2 Step 2. Translate the crate into Lean The crate, spec included, is translated into Lean by our forks of Charon [2] and Aeneas [3]. Aeneas turns safe Rust into pure Lean functions. A &mut argument becomes a value that goes in and a value that comes out, which is sound because Rust’s ownership rules guarantee nobody else can touch that value while the reference is alive. A loop becomes a recursive body function. Every arithmetic operation returns a Result, so an overflow that would panic in Rust becomes a fail in Lean. The output is a Lean program with the same meaning as the crate. The spec’s helper functions are handled differently. Instead of going through Aeneas, the #[pure] macro rewrites their Rust bodies directly into Lean definitions, and after the translation our driver inserts those definitions into the Lean program. So reverse_spec_helper arrives in Lean as an ordinary recursive definition, one a proof can unfold and do induction on. 3.3 Step 3. Turn the spec into a theorem At this point the Lean program contains the implementation, the helper functions, and the spec. The spec is then turned into a theorem statement by #derive_spec, a Lean command we wrote. For reverse_vc_spec the statement fits on one line: ⬇ theorem reverse_vc_spec_correct (x : I32) (hreq0 : decide (core.num.I32.MIN ≤ x) = true) (hreq1 : decide (x ≤ core.num.I32.MAX) = true) : ∃ r, reverse_vc_spec x = ok r The theorem says that for any x in range, reverse_vc_spec x returns a result. A failed ensures would make it return an error instead, so returning a result means the postcondition held. Inputs whose reversal does not fit need no special treatment. Both the code and reverse_spec give 0 for them, so the postcondition also holds. Each #[spec] function becomes one theorem. Many problems have more than one, since a postcondition with a quantifier is stated as its own #[spec] function. The 1007 problems give 1325 theorems in total. 3.4 Step 4. Prove the theorems Proving the theorems happens in three stages, each picking up what the previous one left. Automation proves what it can. A fixed sequence of Lean tactics runs on every theorem first. When it fails it leaves behind the exact goal it could not close. Agents write the rest. The agents work in a repository that holds, for each problem, the Rust code, the problem’s description, the restated specification, and the Lean translation ending in the theorem with its proof left as sorry. An agent takes one theorem at a time and works out everything the proof needs. It has three hours and 40 iterations, each of which submits the current proof to Lean and returns the errors to revise against. It may not touch the code or the statement. If it believes the theorem is false, it releases it with its reason. The gate decides what counts. Every proof goes through the same check. The theorem statement and the generated part of the file must be byte-identical to the originals, and Lean must report no axioms beyond its three standard ones (propext, Classical.choice, Quot.sound). sorry, admit, native_decide and bv_decide are forbidden. Every accepted proof is re-checked from scratch in a clean clone, and a proof that fails the re-check counts as unproved. When nothing closes a theorem, it stays open, with the agent’s notes recorded for the next attempt. For reverse, most of the work is a lemma about the loop, proved by induction with this invariant, quoted from the accepted proof: ⬇ inv := fun (s : I32 × I32) => 0 ≤ s.1.val ∧ 0 ≤ s.2.val ∧ s.2.val ≤ 2147483647 ∧ reverse_spec_helper_pure s.1.val.toNat s.2.val.toNat = target The state s is the pair of cur and res from the code. The invariant says both stay non-negative, res stays within i32, and continuing from this state ends at the expected answer. The rest of the proof handles the code outside the loop and applies the lemma. The agent wrote 198 lines of Lean in all. The benchmark’s own Verus proof states essentially the same invariant. 4 Results 4.1 Specification translation All 1007 specifications were translated, 768 by the transpiler and 239 by agents running on Claude Opus 5.5. To validate them, we ran each translated spec, which is executable Rust, against the benchmark’s test suites. It must accept every correct case and reject every mutated case. This validated 658 of the 1007 specs. The other 349 could not be checked by the test suites, and an agent reviewed them against the Verus original under a written protocol. • 134 have a quantifier the check cannot enumerate and 44 are extended problems with no suite. We sampled 20 specs from each group and reviewed them. • 169 had a suite that could not finish and were all reviewed one by one. 23 of those were sampled for a second review that is not given the first verdicts. • For the remaining 2, special-judge problems whose suites accept several answers, we checked every answer our spec accepted against the benchmark’s own specification, and all were valid. The reviews found no wrong or weakened spec. 4.2 Code translation All 1007 programs translate to Lean, and every theorem statement is covered. To validate the translation, we executed the generated Lean definition of the program on the benchmark’s own test cases and compared the results with the Rust program’s. We ran the 21,413 test cases shipped with 114 of the problems, and all of them passed. For 27 problems, the specification or the code could not be translated as it stood, and we made a specialization to get the translation through. The benchmark’s code or a spec helper was re-encoded in a form the toolchain or the spec crate could handle, with evidence that the meaning is unchanged. Appendix A lists them. 4.3 Proof generation All 1325 theorems were proved, and every proof passed the re-check. That is every theorem of every one of the 1007 problems. 1259 of the proofs were written by Claude Opus 5.5 over just under 32 hours, with three agents working in parallel. The other 66 came from earlier runs and were re-checked against the current statements. 50 were from a pilot on the first fifty problems, written by Claude Fable 5.1 and Claude Opus 5.5, 10 from a trial on the hardest problems, written by Opus 5.5, and 6 were written as worked examples for the agents’ instructions. Table 2 gives the figures for those 1259 proofs. Per proof Median Mean 90th percentile Max Time, claim to submit 3.2 min 4.1 min 7.7 min 69.7 min Iterations (budget 40) 1 1.47 3 7 Cost $1.17 $1.28 $2.22 $5.67 Table 2: The 1259 proofs of the main run. A typical proof took an agent about three minutes from claiming the theorem to submitting the proof, and nine in ten took under eight minutes. The slowest took just over an hour. For comparison, the 60 proofs from the pilot and the trial took a median of 21 minutes each, under an earlier version of the instructions and with no other proofs to draw on. Most proofs were right at the first iteration. 888 of the 1259 were accepted on the first iteration, 231 on the second, 87 on the third, and the remaining 53 within seven. No proof came near the budget of 40. A proof cost about a dollar at Claude Code’s list prices, and the most expensive about six. The whole run cost $1,615 and delivered 39.7 proofs per hour. We gave each problem a rough difficulty estimate. Harder problems took longer and cost more, but the gap is small (Table 3). The hardest class took under 3x the time and money of the easiest, and no more iterations. Difficulty changed the price of a proof, not whether we got one. Difficulty Proofs Median time Mean iterations Median cost 0 to 50 400 2.4 min 1.64 $0.87 50 to 100 250 3.2 min 1.36 $1.20 100 to 200 298 3.9 min 1.44 $1.35 200 to 400 204 4.7 min 1.37 $1.47 400 and up 48 6.9 min 1.23 $2.20 Table 3: The main run’s proofs by difficulty estimate. 4.4 Models and reasoning effort The run used Claude Opus 5.5 at one reasoning-effort setting. We wanted to know how much that choice mattered, so we repeated a small part of the run with four Claude models and four GPT models at five effort settings each. We took 10 theorems from the run, spread across its range of difficulty. Opus had spent between 1.1 and 9.7 minutes on them. Each model at each setting attempted each theorem once, alone in a fresh environment with only the theorem and the instructions, and with a budget of 10 iterations and three hours. The GPT models ran through Codex. We stopped running Haiku on the hardest theorems after it failed the easier ones, so it made 43 attempts in place of 50. Table 4 shows how many theorems each model proved and Table 5 the cost per proved theorem. Theorems proved low medium high xhigh max Claude Claude Fable 5.1 10 of 10 10 of 10 10 of 10 10 of 10 10 of 10 Claude Opus 5.5 10 of 10 10 of 10 10 of 10 10 of 10 10 of 10 Claude Sonnet 5.5 9 of 10 10 of 10 10 of 10 10 of 10 10 of 10 Claude Haiku 4.5 0 of 9 0 of 8 0 of 9 0 of 8 0 of 9 GPT GPT-6 Astra 10 of 10 10 of 10 10 of 10 10 of 10 10 of 10 GPT-6.1 Sol 10 of 10 10 of 10 10 of 10 10 of 10 10 of 10 GPT-6 Sol 9 of 10 10 of 10 10 of 10 10 of 10 10 of 10 GPT-6 Luna 0 of 10 0 of 10 3 of 10 8 of 10 8 of 10 Table 4: Theorems proved by model and reasoning-effort setting. Fable, Opus, GPT-6 Astra and GPT-6.1 Sol proved every theorem at every setting. Sonnet and GPT-6 Sol proved all but one, each missing it at low effort. GPT-6 Luna proved nothing below high effort and 8 of 10 at the top two settings. Haiku proved none. For the models that succeeded, the median number of iterations per proof was one at every setting, except GPT-6 Astra and GPT-6 Sol at low effort, which needed two and three. More effort bought more proofs only for Luna. Cost per proved theorem low medium high xhigh max Claude Claude Fable 5.1 $3.59 $4.71 $5.41 $7.40 $7.97 Claude Opus 5.5 $1.20 $1.43 $1.56 $2.22 $3.57 Claude Sonnet 5.5 $0.95 $0.94 $0.97 $1.40 $2.56 GPT GPT-6 Astra $2.38 $2.21 $2.28 $2.69 $2.99 GPT-6.1 Sol $0.39 $0.40 $0.39 $0.44 $0.49 GPT-6 Sol $1.20 $1.00 $1.02 $1.18 $1.32 GPT-6 Luna – – $0.19 $0.17 $0.22 Table 5: Cost per proved theorem. GPT costs are estimates at API list prices from the tokens reported, since those runs went through Codex. More effort did raise the bill. For the Claude models the highest setting cost 2x to 3x the lowest, and took longer. For the GPT models the rise was a quarter or less. GPT-6.1 Sol was the cheapest at about $0.40 a proof, Sonnet about a dollar, and Fable the most expensive. Median times were 4 to 8 minutes a proof for Opus and Sonnet, 5 to 8 for GPT-6 Astra, and 17 to 21 for GPT-6 Sol. Ten theorems is a small sample with few hard ones in it, so we read these figures as indications. Among the Claude models, Sonnet at low effort was the cheapest setting. Does it hold up on hard theorems? We took the 50 theorems the run had spent the most time on. Opus had taken between 10 and 70 minutes on each. We gave each to Sonnet at low effort under the same conditions as before, alone with the theorem and the instructions, 10 iterations and three hours. The instructions had been revised in the meantime with lessons from the run. Table 6 gives the outcome. Sonnet 5.5 at low effort, 50 hardest theorems Proved 50 of 50 Accepted on the first iteration 48 of 50 Median time per proof 16.3 min Median cost per proof $2.17 Total cost $118 Table 6: Sonnet 5.5 at low effort on the 50 theorems the run spent the most time on. Sonnet proved all fifty, 48 of them at the first iteration. On the same fifty theorems in the run, Opus had a median of 13.8 minutes and $2.73 a proof, with 44 at the first iteration. Sonnet was cheaper on 38 of the 50 and slower on most, taking about 1.3x as long. The two runs differ in more than the model, so this is not a controlled comparison. It does say that the hardest theorems in the benchmark are within reach of the smaller model at its lowest effort setting. 4.5 Comparison with the VeriContest paper Our results and the results the VeriContest paper reports for frontier models are not strictly comparable, for two reasons. 1. The VeriContest paper reports pass@1. Each model is asked once for a proof and that single output is checked. Our agents get up to 40 iterations of checking and revising, with Lean’s feedback after each. 2. The models are different. The highest ProofGen score in the VeriContest paper is GPT-5.5’s, and our agents run on Claude Opus 5.5. So we ran the paper’s own ProofGen task ourselves with Claude Opus 5.5, following the setting the benchmark suggests. We allowed 10 iterations and three hours per problem, since no proof in our run needed more than 7 iterations. We ran it on the 50 problems whose reference proofs are the longest in the benchmark, from 527 to 1,777 added lines. Table 7 gives the outcome. Opus 5.5, 50 longest reference proofs Total Median Mean 90th pct. Max Proved 49 of 50 Accepted on the first attempt 18 of 50 Time per proof 6.1 min 7.4 min 12.0 min 26.7 min Iterations per proof (budget 10) 2 2.31 4.2 10 Cost per proof $0.92 $1.12 $2.05 $4.14 Table 7: The benchmark’s own Verus protocol, run with Claude Opus 5.5. Time is from the first request to acceptance. Our run proved all 1325 theorems. For the 1259 the main run wrote, 70 % were accepted on the first iteration, at a median of 3.2 minutes and $1.17 per proof. Opus 5.5 under the paper’s protocol proved 49 of these 50 problems, 36 % on the first attempt, at a median of 6.1 minutes and $0.92 per proof. There is one difference the numbers do not show. Ours are Lean proofs, mathematical objects that anyone can re-check with nothing but the file. A Verus pass is a solver’s verdict, and it cannot be re-checked outside Verus. If anything, the comparison is tilted against us, for two reasons. 1. Coverage. Our run covers all 1007 problems and all 1325 theorems. This one covers 50 problems. 2. The risk of label leakage. The benchmark’s reference proofs in Verus have been public on GitHub since the paper came out in May 2026, and Opus 5.5 is newer than that. A model asked for a Verus proof may have seen the published answer. Our run is far better placed. No Lean proof of any of these theorems existed anywhere before we wrote them, so there was no answer to recall and every proof had to be found. What remains is indirect. The Rust code and its Verus proof are public, and a model that studied the code may remember an invariant the Verus proof used. That is a hint at most, not a proof, and it still had to be turned into a Lean proof that the kernel accepts. 5 Conclusion Every theorem of every VeriContest problem now has a Lean proof, written by agents at a median of three minutes and about a dollar each, and checked by Lean’s kernel with no axioms beyond the standard three. The benchmark’s authors found proof generation to be the bottleneck for frontier models. With Lean’s feedback to iterate against, it is not. Three questions remain open. 1. How much of this carries over to the crates we verify for customers. There the specifications are written from scratch, not restated from a benchmark. 2. How far the cheapest settings go. Sonnet at low effort proved the hardest fifty theorems. 3. How much a model’s score on a public benchmark owes to having seen its answers. The benchmark’s Verus proofs are public, so for the Verus rerun this cannot be ruled out. No Lean proof of these theorems existed before we wrote them, so our run is far better placed, as Section 4.5 discusses. References [1] L. de Moura and S. Ullrich (2021) The Lean 4 theorem prover and programming language. In Automated Deduction (CADE-28), Cited by: §1. [2] S. Ho, G. Boisseau, L. Franceschino, Y. Prak, A. Fromherz, and J. Protzenko (2025) Charon: an analysis framework for Rust. In Computer Aided Verification (CAV), Cited by: §3.2. [3] S. Ho and J. Protzenko (2022) Aeneas: Rust verification by functional translation. Proceedings of the ACM on Programming Languages 6 (ICFP). Cited by: §3.2. [4] 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. Proceedings of the ACM on Programming Languages 7 (OOPSLA1). Cited by: §1. [5] Z. Xie, M. Pawagi, Y. Liu, A. Rai, L. Shao, J. Berberian, S. Che, and W. Wang (2026) VeriContest: a competitive-programming benchmark for verifiable code generation. External Links: 2605.08553 Cited by: §1. Appendix A The 27 specializations Specialization Problems What was done Why Evidence of unchanged meaning Implementation rewritten 2 (lc3046, lc3233) A nested for with an early return became a while. f64::sqrt became an integer floor square root. Specs unchanged. The translation could not join that loop’s exits. No floating-point model. Exhaustive or differential testing against the old code. Review. Spec helper redefined 1 (lc1700) A helper that rotates a queue was redefined as a counting model. Code unchanged. No list construction in the spec crate. Equivalence proof by induction. 420,000-case differential test against the Verus helper. The test suites. Review. Strings as bytes 17 (ASCII string problems) String and Vec<char> became Vec<u8>, character literals became bytes, in code and spec. Suite strings are fed in as bytes. No char type in the spec crate. Each problem’s precondition restricts inputs to ASCII, so nothing is lost. Differential test against a Vec<char> transcription. Review. Pairs as parallel vectors 5 (cf437C, cf479C, cf1788C, lc163, lc885) A Vec<(A, B)> became two vectors of equal length, in code and spec. No tuple element types in the spec crate. Bijection argument per problem. Differential test against a tuple transcription. Review. Hash maps as vectors 2 (lc421, lc523) A HashSet and a HashMap became vector lookups with the same contents at every step. Specs unchanged. Standard hash maps bring opaque hasher axioms into the translation, so no proof over them is kernel-clean. Same result by construction. Review. Table 8: The 27 problems whose code or spec helper was re-encoded to get the translation through.