Source-linked AI summary
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora
TL;DR
Existing benchmarks provide limited evidence about LLMs’ ability to verify classical algorithms requiring global reasoning, and cross-language comparisons are often misaligned. AlgoVeri evaluates 77 aligned problems in Dafny, Verus, and Lean. The paper reports different performance and repair dynamics across verification systems and model types.
Problem
Existing benchmarks often omit classical algorithms requiring global reasoning, while cross-language suites may compare different tasks or specification difficulty.
Source: §1 · pp. 1–2Method
AlgoVeri evaluates 77 classical algorithm problems using semantically aligned specifications across Dafny, Verus, and Lean.
Source: §1 · p. 2, §2.3 · p. 3Results
Takeaways & Limitations
The benchmark reveals a language hierarchy in which Dafny is currently more viable for LLMs than Verus and Lean, while frontier models make more effective use of reasoning depth than current open models.
Source: §6 · p. 9Verified programs are correct only with respect to their specifications, so specification validity and completeness still require human oversight.
Source: Impact Statement · p. 9
Abstract
from arXiv · showhide
Vericoding refers to the generation of formally verified code from rigorous specifications. Recent AI models show promise in vericoding, but a unified methodology for cross-paradigm evaluation is lacking. Existing benchmarks test only individual languages/tools (e.g., Dafny, Verus, and Lean) and each covers very different tasks, so the performance numbers are not directly comparable. We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean. By enforcing identical functional contracts, AlgoVeri reveals critical capability gaps in verification systems. While frontier models achieve tractable success in Dafny ($40.3$% for Gemini-3 Flash), where high-level abstractions and SMT automation simplify the workflow, performance collapses under the systems-level memory constraints of Verus ($24.7$%) and the explicit proof construction required by Lean (7.8%). Beyond aggregate metrics, we uncover a sharp divergence in test-time compute dynamics: Gemini-3 effectively utilizes iterative repair to boost performance (e.g., tripling pass rates in Dafny), whereas GPT-OSS saturates early. Finally, our error analysis shows that language design affects the refinement trajectory: while Dafny allows models to focus on logical correctness, Verus and Lean trap models in persistent syntactic and semantic barriers. All data and evaluation code can be found at https://github.com/haoyuzhao123/algoveri.
1. Introduction
Existing benchmarks leave open whether LLMs can verify classical algorithms requiring global reasoning and make fair cross-language comparisons difficult. AlgoVeri aligns 77 algorithmic problems across Dafny, Verus, and Lean and uses the benchmark to examine performance and failure dynamics.
1. Introduction
- Existing benchmarks often omit global-property reasoning and lack fair cross-language comparisons because tasks or specification difficulty differ across tools.For example, proving a red-black tree insertion correct requires preserving its global black-height property.Source: §1 · pp. 1–2
- The benchmark evaluates implementations and proof artifacts through iterative compiler refinement, then uses an LLM judge to check whether verified code implements the intended algorithm.The semantic check guards against verified but unintended behavior.Source: Figure 1 · p. 2, §1 · p. 2
- AlgoVeri aligns 77 classical algorithm problems across Dafny, Verus, and Lean to support comparisons of deep reasoning across verification systems.The suite spans data structures, sorting, graph algorithms, dynamic programming, greedy problems, and selected mathematics algorithms.Source: §1 · pp. 2–3
- Models struggle with graph problems involving ghost state and global reasoning, while more automated Dafny generally achieves higher success rates than Verus and Lean.Verus adds memory-detail burdens, while Lean requires explicit proof guidance.Source: §1 · p. 2
- The paper compares test-time compute allocated to iterative repair versus parallel sampling, finding frontier-model gains across 15 repair rounds while open models saturate early.For current open models, repair is inefficient relative to parallel sampling.Source: §1 · p. 2
- Frontier models improve through repeated feedback, but current open models struggle, and language design shapes where models get stuck.Dafny lets models focus on logical correctness; Verus syntax and Lean proof-step search are persistent barriers.Source: §1 · p. 3
2. ALGOVERI Benchmark
ALGOVERI evaluates vericoding on classical algorithms whose correctness depends on global properties, using aligned specifications across Dafny, Verus, and Lean. It combines expert specification review with formal checks and a pipeline that filters verifier-accepted outputs for algorithmic intent.
2.1. Verified Coding Tasks: Background and Setting
- Classical algorithms require reasoning about global properties such as graph reachability and data-structure invariants, often using ghost state to track auxiliary information.Examples include tracking visited nodes or permutation structure.Source: §2.1 · p. 3
2.2. Task Suite and Benchmark Composition
- The suite covers textbook algorithms across data structures, graph algorithms, and math-related tasks, with aligned specifications for Dafny, Verus, and Lean.Table 1 contrasts its strict parallel alignment and algorithmic depth with existing benchmarks.Source: §2.2 · p. 3, Table 1 · p. 4
2.3. Specification Validation and Quality Control
- Specifications preserve the same semantic meaning across systems, including a unified global-optimality definition for dynamic programming.This alignment can make specifications non-idiomatic for Lean, imposing translation hardness, but is used to isolate model reasoning.Source: §2.3 · p. 3
- Experts manually write, align, and review specifications because test-based checks can weaken constraints and may miss specification errors.The paper additionally checks representative hard tasks for local satisfiability and whether dropping a clause permits unintended behavior.Source: §2.3 · p. 4
2.4. Evaluation Pipeline
- Models generate implementations and proof artifacts, then may refine them over multiple turns using compiler or verifier feedback.A solution is compiler verified when the verifier accepts its proof artifacts under the specification.Source: §2.4 · p. 4
- An LLM semantic filter checks whether verifier-accepted solutions match the intended algorithm, and results distinguish verification success from end-to-end success.This addresses cases where different algorithms satisfy the same specification, such as bubble sort and merge sort.Source: §2.4 · p. 4
3. Evaluation Results
On ALGOVERI, models achieve limited full correctness, with a steep performance gradient across verification systems. Results also show a fidelity gap between verifier acceptance and intended algorithmic correctness, and greater difficulty on complex problems.
3. Evaluation Results
- The evaluation used 15 repair rounds for representative proprietary and open-weight models, with open-weight models also tested at up to 10 passes of 15 rounds.The paper reports results across Dafny, Verus, and Lean.Source: §3 · p. 4
- 40.3% full correctness in Dafny, 24.7% in Verus, and 7.8% in Lean were achieved by Gemini-3 Flash with a 15-round repair budget.The reported benchmark results show a steep difficulty gradient from Dafny to Lean.Source: §3 · p. 4, Table 2 · p. 5
- ≈15% of Gemini-3 Flash's Dafny solutions dropped from compiler verified to compiler verified and semantically filtered, illustrating the algorithmic-fidelity gap.Observed failure modes include exploiting assumptions or sorry and implementing simpler algorithm variants.Source: §3 · p. 5
- Models perform decently on basic data structures and sorting but struggle more on advanced data structures and graph algorithms, particularly in Verus and Lean.The missing regions correspond to tasks requiring auxiliary state or complex global properties.Source: §3 · p. 5
4. Ablations, Analysis and Discussion
The analysis finds that frontier models improve through repeated feedback, while open models saturate early; verification systems also shape whether models get stuck on syntax or proof steps.
4. Ablations, Analysis and Discussion
- Repeated feedback improves frontier-model solutions, while open models saturate early and verification systems determine whether failures center on syntax or proof steps.The section examines iterative repair and parallel sampling, then analyzes failure modes across systems.Source: §4 · p. 5
4.1. The Scaling Laws of Verification: Depth vs. Width
- Gemini-3 Flash improves continuously on Dafny and Verus, nearly tripling its Dafny pass rate from Round 0 to 15 by using compiler feedback to fix complex errors.The verifier acts as a constructive reward signal during repair.Source: §4.1 · pp. 5–6
- GPT-OSS-120B saturates early, typically by Round 3, with negligible gains from further repair as deeper verification failures persist.The authors suggest the open model lacks the reasoning depth for multi-turn repair chains.Source: §4.1 · p. 6
- At equal generation budgets, GPT-OSS-120B repair fails to significantly outperform parallel sampling and often degrades performance, favoring compute scaled with width over depth.The comparison uses N one-round samples versus N/15 chains of 15 repair rounds.Source: §4.1 · p. 6
4.2. The Anatomy of Failure: Language Barriers
- Dafny repair quickly clears syntax and type errors, leaving the model to refine logical correctness through invariants and assertions.This lets the model produce valid code early and focus on logic rather than basic syntax.Source: §4.2 · pp. 6–7
- Verus retains syntax and type errors throughout repair, with Rust macro syntax and verification rules contributing to a barrier before algorithm verification.Models repeatedly fix syntax or type errors instead of progressing on algorithm verification.Source: §4.2 · p. 7
- Lean failures combine hallucinated lemmas with verification errors, requiring models both to retrieve valid proof steps and apply them correctly.The authors characterize this as a joint search and reasoning challenge.Source: §4.2 · p. 7
4.3. Implications: The Case for Heterogeneity
- The discussion frames three reasons to target Verus or Lean despite Dafny’s superior benchmark performance.It introduces a case for heterogeneous verification systems.Source: §4.3 · p. 7
1. The trust vs. automation trade-off (SMT vs. ITP).
The section weighs SMT automation against interactive theorem proving by contrasting trust, performance on complex invariants, and implementation-level constraints.
1. The trust vs. automation trade-off (SMT vs. ITP).
- Dafny’s high automation relies on the soundness of a large SMT solver trusted base, while Lean’s small trusted kernel offers a higher assurance standard but less automation.The passage identifies Z3 as an example SMT solver.Source: §1 · p. 8
- For complex graph invariants, performance converges to near-zero across paradigms, suggesting SMT automation is not a silver bullet and motivating explicit proof construction in interactive provers.The authors argue that restricting tools to SMT would ignore interactive provers’ fine-grained manual control.Source: §1 · p. 8
- Dafny’s unbounded integers and managed memory ease verification, whereas Verus enforces ownership and fixed-width integers with verbose syntax, compounded by scarce training data (Chen et al., 2024; Shefer et al., 2025).The authors caution that lower Verus performance reflects distinct constraints of efficient executable systems code.Source: §1 · p. 8
5. Related Work
Prior verified-code benchmarks often trade algorithmic depth against verification rigor or cross-language comparability. AlgoVeri positions aligned specifications as a basis for comparing approaches to vericoding classical algorithms.
5. Related Work
- Existing benchmarks often emphasize particular verification settings: DafnyBench focuses on annotation reconstruction, while CLEVER and Verina test rigorous protocols on introductory coding tasks.VeruSAGE targets systems correctness, and VeriCoding’s translations can introduce semantic drift.Source: §5 · p. 8
- AlgoVeri aligns specifications for the same data structures and algorithms across Dafny, Verus, and Lean, enabling controlled comparisons of how formal systems shape reasoning.Its target is textbook algorithmic complexity.Source: §5 · p. 8
- Research spans specialized training and inference-time repair, but remains fragmented; AlgoVeri offers a unified testbed for comparing specialized training with generalist reasoning.Examples include Re:Form’s reinforcement learning for Dafny and Copra’s prove-and-repair workflow.Source: §5 · p. 8
- Math-prover advances do not transfer straightforwardly to algorithm verification, which requires reasoning about imperative state, mutable memory, and termination.The benchmark can compare math-inspired search, specialized training, and generalist repair on state-heavy algorithmic correctness.Source: §5 · pp. 8–9
6. Conclusion
The conclusion presents ALGOVERI as an aligned benchmark for vericoding across Dafny, Verus, and Lean. It reports a language hierarchy and contrasting test-time compute patterns across frontier and open models.
6. Conclusion
- ALGOVERI aligns specifications across Dafny, Verus, and Lean to disentangle problem difficulty from tool-chain effects.It is a multi-lingual benchmark for vericoding.Source: §6 · p. 9
- Dafny currently offers the most viable path for LLMs, while Verus syntax burdens and Lean’s proof-search space remain significant barriers.The hierarchy reflects high-level SMT automation in Dafny versus systems-level verification and interactive theorem proving.Source: §6 · p. 9
- Frontier models leverage reasoning depth for repair, whereas open models saturate early and benefit more from parallel sampling.The conclusion frames ALGOVERI as useful for distinguishing reasoning progress from syntactic proficiency.Source: §6 · p. 9
Impact Statement
AlgoVeri aims to make formal verification more accessible, potentially supporting high-assurance guarantees for critical infrastructure. The authors caution that verified code is only correct relative to its specification, making specification validity and completeness important targets for human oversight.
Impact Statement
- ALGOVERI aims to make formal methods easier and potentially enable high-assurance guarantees for critical infrastructure that is costly to verify manually.The stated aim is to benchmark and improve LLMs’ ability to generate verified code.Source: Impact Statement · p. 9
- Verification does not guarantee that the specification itself is correct.As verification becomes more accessible, the authors say oversight should focus on specification validity and completeness.Source: Impact Statement · p. 9
- The authors recommend treating neuro-symbolic tools as reliability assistants, not replacements for rigorous system design.They report no obvious negative social impact while emphasizing this boundary.Source: Impact Statement · p. 9
A. Background on Program Verification
The background distinguishes verified code generation from test-based generation and explains the components of a verified program. The examples frame the specification, executable implementation, and proof artifacts as separate parts of the task.
A.1. The Anatomy of a Verified Program
- Verified code generation requires an implementation, specification, and proof artifacts, rather than code that merely passes finite input-output tests.The paper illustrates these components with Linear Search examples in Dafny, Verus, and Lean.Source: §A.1 · p. 12
- A specification defines correctness for all valid inputs through preconditions, postconditions, helper definitions, and a function signature.The passage contrasts this contract with a unit test that checks a specific value.Source: §A.1 · p. 12
- The implementation is the executable solution logic, such as a while loop or a recursive definition.The paper identifies this component as the part most similar to standard pre-training data.Source: §A.1 · p. 12
- Proof artifacts are non-executable annotations that convince the verifier the implementation satisfies the specification.Examples include loop invariants, ghost code, and tactics that guide the prover.Source: §A.1 · p. 12
A.2. Verification Paradigms: The Syntax vs. Search Barrier
This section describes verification barriers, the benchmark’s stricter-than-execution success criterion, tested models, and the prompts used for generation, repair, and semantic checking.
A.2. Verification Paradigms: The Syntax vs. Search Barrier
- The systems are grouped by the artifacts models must produce: SMT-based Dafny and Verus use invariants and ghost proofs, while Lean uses tactic scripts.Dafny and Verus guide an SMT solver with assertions; Lean proofs are constructed interactively by tactics.Source: §A.2 · p. 15
- Verus imposes a pronounced syntax barrier because models must bridge Rust’s low-level types and mathematical logic, including explicit type conversions.A missing conversion can cause verification failure even when the logical reasoning is correct.Source: §A.2 · p. 15
B. Detailed Model Information
- Table 3 lists the models tested in Sections 3 and 4.The supplied caption identifies the table’s scope but does not specify its model entries.Source: Table 3 · p. 16
A.2. Verification Paradigms: The Syntax vs. Search Barrier
- Lean presents a search barrier: the model must choose tactics that navigate proof states toward a completed proof.The example sequence unfolds a definition, extracts a property, simplifies the goal, and closes it.Source: §A.2 · p. 16
A.3. Verification vs. Execution
- A benchmark submission succeeds only when a verifier certifies correctness for all possible inputs, not merely when code passes finite tests.Correct executable code can still fail if its proof artifacts, such as a loop invariant, are missing.Source: §A.3 · p. 16
C. Prompt Templates
- The prompt framework uses an initial interaction, multi-turn revision, and a final semantic check to filter cheating and algorithmic degeneration.The section includes initial and follow-up prompts for the verification systems and for semantic validation.Source: C. Prompt Templates · p. 16
C.1. Prompt Templates for Dafny
- Dafny prompts ask for a complete implementation and proof while preserving the supplied preamble, signature, and specification.The prompt requests high-level reasoning and a plan before the standalone Dafny code.Source: §C.1 · p. 17
C.2. Prompt Templates for Verus
- Verus prompts ask for complete Rust code and proof while retaining the supplied preamble, signature, and specification.The prompt also requests reasoning and planning and prohibits specified verification-bypass constructs.Source: §C.2 · p. 18
D. Detailed Specification Examples
The specification examples illustrate ALGOVERI’s cross-language alignment and algorithmic rigor through a dynamic-programming problem and a complex graph problem.
D. Detailed Specification Examples
- The examples are presented to demonstrate strict alignment across languages and algorithmic rigor in ALGOVERI’s specifications.The section introduces Longest Increasing Subsequence and Max Flow as representative problems.Source: D. Detailed Specification Examples · p. 21
- The Longest Increasing Subsequence example contrasts ALGOVERI with VeriCoding and highlights how aligned specifications avoid trivial safety-only proofs.It is presented as a standard dynamic-programming problem.Source: D. Detailed Specification Examples · p. 21
- The Max Flow example requires reasoning about global graph invariants and existential witnesses for optimality.It uses the Edmonds-Karp algorithm as a complex graph example.Source: D. Detailed Specification Examples · p. 21
D.1. Comparison of Specifications: ALGOVERI vs. VeriCoding
The LIS specifications contrast AlgoVeri’s aligned functional contracts with VeriCoding’s inconsistent standards across languages. AlgoVeri requires global correctness, while VeriCoding’s Dafny and Verus checks omit algorithmic logic and its Lean check is harder.
D.1. Comparison of Specifications: ALGOVERI vs. VeriCoding
- AlgoVeri aligns the Dafny, Verus, and Lean contracts through equivalent validity predicates and postconditions requiring a valid subsequence of maximum length.The contracts require both a valid subsequence matching the result and proof that no longer valid subsequence exists.Source: §D.1 · p. 21
- VeriCoding’s Dafny and Verus specifications check only result bounds, while its Lean specification checks full functional correctness, creating an uneven evaluation standard.The Dafny and Verus checks could be satisfied by returning 0.Source: §D.1 · p. 21
Longest increasing subsequence problem in ALGOVERI
- For LIS, the postcondition requires an actual valid increasing subsequence of the returned length and bounds every valid subsequence by that length.The validity predicate includes increasing indices, in-range indices, and increasing values.Source: Longest increasing subsequence problem… · p. 24
D.2. Example Specifications of Max Flow in ALGOVERI
These examples specify Max Flow across Dafny, Verus, and Lean, aligning helper predicates and requiring a valid concrete flow witness that is maximal. The Lean example specifies Edmonds–Karp with a capacity graph, explicit flow values, preconditions, and a postcondition tying the returned value to a maximum flow.
D.2. Example Specifications of Max Flow in ALGOVERI
- The specification requires global flow invariants, including capacity constraints, flow conservation, and optimality.The flow witness must satisfy validity constraints and be maximal.Source: §D.2 · pp. 25–26
- Dafny, Verus, and Lean Max Flow specifications use identical helper predicates to maintain strict alignment.The examples formalize the Edmonds–Karp algorithm.Source: §D.2 · p. 26
- The postcondition requires an existential flow map whose value equals returned max_val and whose flow is provably maximal.This prevents solutions that merely return a lucky guess.Source: §D.2 · pp. 26, 28
- The specification models a capacity graph and uses an explicit function-valued FlowMap to assign integer flows to node pairs.The passage contrasts explicit flow values here with abstract or implicit paths used in other examples.Source: §D.2 · p. 31
- A maximum-flow map respects edge capacities and is nonnegative; its flow value is at least that of every other valid flow for the same source and sink.Flow value is defined as flow out of the source minus flow into it.Source: §D.2 · pp. 31–32
- The precondition requires a well-formed graph with bounded capacities, in-range distinct source and sink nodes, and the postcondition requires a maximum-flow witness matching the result.Graph size is at most 1000 and each edge capacity is between 0 and 100000.Source: §D.2 · p. 32
- The example leaves both the max_flow_value implementation and its postcondition proof as sorry placeholders.The code includes a theorem asserting that the postcondition is satisfied under the stated precondition.Source: §D.2 · p. 32