AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and main result

AlgoVeri is a benchmark paper, not a new verifier. It studies whether a language model can produce an implementation and proof artifacts, against a provided formal specification, for 77 textbook algorithms in three systems: Dafny, Verus, and Lean 4. The paper defines vericoding as “Vericoding refers to the generation of formally verified code from rigorous specifications.” (Abstract, p. 1). Its central experimental control is semantic alignment: the same algorithmic contract is expressed in each language, so a difference in pass rate is attributed more plausibly to the toolchain or model than to an easier task. The suite includes sorting, advanced data structures, dynamic programming, and graph algorithms such as Edmonds–Karp. These require global invariants, ghost state, and termination reasoning rather than only local array bounds.

The practical finding for VL (VeruLaw, agents writing Rust verified with Verus) is a large gap between compiling and delivering the intended algorithm. Gemini-3 Flash, with 15 repair rounds, obtains 25.97% compiler-verified Verus submissions and 24.68% after semantic filtering (77 tasks, Table 2). GPT-5.3 Codex obtains 14.29% and 11.69% respectively with eight rounds. Dafny is higher (Gemini 55.84% compiler verified, 40.26% filtered), while Lean is lower for Gemini (9.09% and 7.79%; GPT-5.3 Codex reaches 23.38% compiler verified and 11.69% filtered in Lean). These are percentages over the 77 benchmark problems; the paper does not present confidence intervals for the proprietary-model rows.

technique 1: align one contract across languages

What it is: construct one corpus of algorithm problems, then manually encode semantically equivalent helper definitions, preconditions, and postconditions in Dafny, Verus, and Lean. The paper says the suite “A LGOV ERI contains aligned specifications across Dafny, Verus, and Lean.” (Section 2.3, p. 3). Alignment means that a dynamic-programming contract uses the same global optimality definition, and a max-flow contract requires capacity, conservation, and maximality, not merely a bounded return value.

When to use it: use this design whenever a benchmark compares proof systems or models. Without it, high scores can result from weak contracts in one language. For example, the paper contrasts its longest-increasing-subsequence contract (existence of a valid subsequence of the returned length and impossibility of a longer one) with an earlier Dafny/Verus contract that accepts result 0 because it only checks bounds.

How to do it:

1. Choose the textbook algorithm and write its natural-language requirements, including algorithm identity or complexity when these matter.
2. Define language-independent predicates. In the LIS example, is_valid_is requires increasing indices, in-range indices, and strictly increasing values.
3. Translate those predicates into each verifier while preserving quantifier meaning. The max-flow example defines respects_capacity, recursive incoming/outgoing sums, is_conserved, is_valid_flow, flow_val, and is_max_flow.
4. Give every implementation the same formal function contract and require an existential witness where a scalar could be guessed. The max-flow postcondition asks for a concrete flow map that is valid, maximal, and has the returned value.
5. Freeze the specifications before model evaluation (the study’s recommendation, not stated in the paper) and report compiler verification and semantic fidelity separately (as the paper does).

Verus form (inference from the paper’s examples): use spec fn predicates over Seq, Map, and integer views (vec@), then put identical requires/ensures in the Rust function. Represent graph state with a CapacityGraph::view specification and use #[trigger] annotations where quantifier instantiation needs help. Unlike Dafny’s unbounded mathematical types, Rust requires explicit casts such as let low_idx: int = low as int; ownership and fixed-width arithmetic remain implementation obligations.

Evidence and limits: strict alignment isolates tool effects, but it is not automatic. The authors manually review specifications and acknowledge that a single mathematical contract can be non-idiomatic in Lean. Alignment therefore measures cross-tool difficulty under a chosen abstraction; it does not prove that each translation is equally natural. The benchmark’s semantic validator is itself an LLM, so algorithm-identity filtering is an additional model-dependent measurement.

technique 2: audit specifications for satisfiability and degeneracy

What it is: combine expert curation with mechanized quality checks. For hard tasks such as Maximum Flow and Tarjan’s SCC, decompose the specification into clauses C_i and prove in Lean (i) local satisfiability—each clause has a witness and is internally consistent—and (ii) necessity against degeneracy—dropping a clause admits an unintended behavior. The paper states that “dropping any Ci admits unintended behaviors (e.g., dropping a permutation constraint allows an arbitrary sorted list)” (Section 2.3, p. 4).

When to use it: run this audit before collecting model scores, especially for quantified contracts and translated specifications. Test-based checks can miss errors because finite tests instantiate only selected values; the paper cites a 10% specification-error rate reported for another benchmark despite test validation.

How to do it (steps 3 to 5 are the study’s elaboration; the paper states only the two Lean conditions and the expert review):

1. Split a contract into independently named semantic clauses (bounds, permutation, monotonicity, conservation, maximality).
2. In a small trusted prover, establish that each clause is satisfiable under the intended preconditions.
3. Remove one clause at a time and search for a model or proof of an undesired implementation; record the counterexample.
4. Repair the contract, rerun the checks, and manually inspect the final aligned definitions.
5. Keep these audits separate from model-generated proof success; they validate the test instrument.

Verus form (inference): write proof lemmas or executable test harnesses that instantiate Seq/Map witnesses for each clause, and maintain explicit ensures that expose the clause. For necessity, a separate specification-level lemma can construct a violating flow or non-permutation sequence when a clause is absent. Verus cannot directly perform the Lean meta-level audit described by the paper; use Lean or another model finder for the benchmark-construction stage, then port the resulting contract to Verus.

Evidence and limits: the paper provides examples and the aligned code, but does not report the number of rejected or repaired specifications. Thus the audit method is reproducible in shape, while its coverage is not quantified. Expert review remains trusted.

technique 3: prove-and-repair with semantic validation

What it is: evaluate a model in a fixed iterative loop. The model receives a problem, formal contract, and incomplete code; it emits implementation plus proof artifacts. The compiler or verifier returns diagnostics; the model revises the submission for up to 15 rounds. A submission first counts as compiler verified, then an LLM judge checks whether it implements the requested algorithm and rejects cheating or degeneracy. This is needed because “a submission succeeds only if the verifier certifies correctness for all possible inputs” (Appendix A.3, p. 16), but compiler acceptance alone can still permit assume/sorry or a simpler algorithm that satisfies an underspecified contract.

When to use it: use the loop for agent training and evaluation when one-shot generation underestimates repair ability. Use a separate semantic check whenever the contract does not encode complexity or algorithm variant.

Steps:

1. Give the model the natural-language task and fixed formal skeleton.
2. Require complete code and proof artifacts, forbidding bypasses.
3. Compile/verify; return the exact diagnostic text.
4. Ask for a full revised file, not a patch, for each round.
5. Record the pass rate per round (Figure 4 plots the average pass rate over repair rounds).
6. Run semantic validation and report both rates.

Verus form (inference): the loop should preserve the verus! wrapper, Rust code, requires/ensures, loop invariant, decreases, and proof {} blocks. Diagnostics should distinguish parser/type failures from failed VCs. A VL agent can use this as a compiler-in-the-loop controller, but must reject assume, admit, unreached, and untrusted external calls before counting success.

Evidence: Gemini’s Dafny pass rate nearly triples from round 0 to 15, indicating useful feedback exploitation; GPT-OSS-120B saturates around round 3. For Gemini’s Verus result, only 24.68% of 77 tasks survive semantic filtering after 15 rounds. Failure remains common despite feedback.

technique 4: choose test-time depth versus width

AlgoVeri treats inference budget as an experimental variable. “The frontier model (Gemini) achieves consistent improvement in both Dafny and Verus as repair depth increases” (Figure 4 caption, p. 6), whereas GPT-OSS shows little gain beyond round 4. Under an equal generation budget, the authors compare parallel one-round samples with fewer chains of 15 repair rounds. For GPT-OSS, deep repair often performs worse than width, suggesting that the model treats diagnostics as resampling context instead of a refinement plan.

Use this measurement when deciding how VL spends expensive inference. Implement an iso-compute sweep: hold total generated tokens or calls fixed, vary chain depth, and report pass rates by verifier. Do not transfer the frontier-model result to open models without measuring; the paper reports an intelligence gap between the frontier and open models.

Verus implication (inference): a VL service can route easy syntax/type fixes through short repair chains, while allocating parallel samples to hard invariant failures. Keep compiler diagnostics attached to each sample and deduplicate equivalent candidates. The study does not establish an optimal policy for Verus specifically; its width-versus-depth conclusion is measured on the listed models and benchmark.

technique 5: classify barriers to target interventions

The paper classifies errors hierarchically, prioritizing syntax and type errors over verification failures (Section 4.2, Figure 6); for Lean it adds a hallucination category. Dafny quickly moves from syntax/type errors to logical invariant failures. Verus retains a “syntax barrier” because Verus is written with Rust macros, so the model must follow Rust’s strict syntax and Verus’s verification rules at once (Section 4.2, p. 7). Lean has a search barrier: models hallucinate lemmas or tactics and then fail to apply valid ones. Inference, not the paper’s claim: the Verus diagnosis suggests investing in Rust/Verus syntax scaffolds, type conversions, and reusable invariant templates before adding more solver heuristics.

A representative Verus proof from Appendix A searches a sorted sequence for a lower bound. The loop maintains bounds, sortedness, and two partition invariants; on the else branch it opens a proof block, casts usize indices to int, and proves the suffix property from sortedness before assigning high = low. The same mathematical argument is written in Dafny with less explicit casting. This example teaches a transferable pattern: separate executable indices from mathematical indices, maintain both sides of a partition, and discharge the branch-specific quantified fact before mutating the boundary.

what is proved, measured, and trusted

The verifier proves each accepted implementation against its supplied contract; it does not prove that the contract captures the intended algorithm. The semantic judge measures algorithmic fidelity, not a kernel theorem. The benchmark construction, cross-language translations, expert reviews, compiler implementations, SMT solver, Lean kernel, and semantic judge are trusted or assumed. Dafny’s automation relies on a larger solver base, while Lean’s kernel is smaller but needs explicit tactic search. The paper itself warns that “A successfully verified program is only correct with respect to its specification; it does not guarantee the correctness of the specifications.” (Impact Statement, p. 9).

contradictions, omissions, and prior work

The headline abstract reports Gemini Verus full correctness as 24.7%, while Table 2 gives 24.68%; this is rounding, not a substantive inconsistency. GPT-5.3’s table row uses an eight-round budget while most rows use 15, so direct model comparisons confound budget. The reported percentages have no denominator printed in each cell, but the benchmark has 77 tasks, making 1/77 approximately 1.30 percentage points. The Gemini-3 Flash cells (1x15) are whole counts of 77: 55.84 is 43, 40.26 is 31, 25.97 is 20, 24.68 is 19, 9.09 is 7, 7.79 is 6; GPT-5.3 Codex 14.29 is 11 and 11.69 is 9 (arithmetic by the study). The Lean 9.09% is Gemini-3 Flash compiler-verified after up to 15 repair rounds in this paper’s own prompt loop (Table 2); the P^3 paper’s 31.2 to 48.1% on AlgoVeri (p_3, Table 2) is a different measure: four other backends (Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, Claude-Opus-4.7) run as Lean agents with Lean tools, with a natural-language complexity instruction added to each task and a task counted only if it satisfies that instruction. Neither paper explains the gap; models, agent tooling and the added instruction differ, so the study cannot attribute it to any one of them. The paper reports no per-task confidence intervals for proprietary models, and the paper does not explain the ± values in Table 2 for the open-model rows.

Earlier benchmarks include DafnyBench (annotation reconstruction), CLEVER and Verina (mostly Lean introductory tasks), VeriCoding (large but unaligned), VeruSAGE (Rust systems), and VerifiedCogen. VL should not redo a basic cross-language benchmark or rely on bounds-only contracts; the reusable contribution is the aligned-contract and degeneracy-audit methodology. What remains open is a rigorous, Verus-native suite with reproducible model prompts, per-task traces, and non-LLM semantic checks.

threat to agent-written verified Rust (inference)

The threat is substantial for functional correctness on global algorithms: current agents pass roughly one quarter of AlgoVeri’s Verus tasks even after 15 repairs, and graph/data-structure cases approach zero in the category plots. A product that accepts only verifier-checked Rust is protected against many implementation bugs, but can still ship an underspecified or degenerate algorithm, misuse assume, or silently fail its intended complexity. The practical mitigations are aligned contracts, clause audits, semantic/complexity validators, strict rejection of bypass constructs, and logging repair trajectories. These are inferences from the benchmark, not claims that AlgoVeri evaluated VL directly.

techniques for the catalog

• aligned cross-language contracts: encode one algorithm’s global predicates and witnesses in Dafny, Verus, and Lean so scores isolate toolchain effects
• satisfiability and degeneracy audit: prove each specification clause is satisfiable and show that removing it permits an unintended behavior
• compiler-in-the-loop prove-and-repair: iterate complete implementation/proof outputs using verifier diagnostics, then apply a separate semantic validator
• iso-compute depth/width evaluation: compare sequential repair chains with parallel samples under equal inference budget
• syntax/search barrier diagnosis: classify parser, type, VC, and tactic-search failures to target language-specific interventions

Audited 2026-10-12 against the paper: checked Table 2 numbers (Gemini 55.84/40.26, 25.97/24.68, 9.09/7.79; GPT-5.3 Codex 14.29/11.69 with 1x8), the abstract figures, quotations and their pages, the Appendix A.3, C and D passages, the LIS, max-flow and lower-bound examples, and the Figure 4 to 6 claims. Corrected: Figure 4 caption page (p. 6); the model produces implementation and proof against a provided specification; Lean figure qualified as Gemini only; intelligence-dependent scaling law replaced by the paper’s intelligence gap; an invented step about recording the first success round; the Figure 6 classification and the syntax barrier cause; an unmarked inference; unsupported repeated runs for the standard deviations; steps that are the study’s own elaboration are now marked. Not checked: the radar-chart category values (Figure 3), the Figure 4 to 6 curves beyond their captions and text, and the 10 percent Verina figure beyond the paper’s own sentence.; follow-up: added 77-task counts behind the table cells (8 versus 15 rounds was already stated) and a clause on what Lean 9.09% measures against the p_3 range.

Last edited: 2026-10-13