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

May combine two claims.

Verus enforces strict implementation-level constraints (e.g., ownership, fixed-width integers), and expressing these constraints requires a verbose and strict syntax that creates a syntax barrier.

“Verus, by contrast, enforces strict implementation-level constraints (e.g., ownership, fixed-width integers).Expressing these constraints requires a verbose and strict syntax that-compounded by the scarcity of Verus training data (Chen et al., 2024;Shefer et al., 2025)-creates a syntax barrier.”

• cites Chen et al., 2024 sourcePartly supported

  Section 3.1 says Verus does not support all Rust features and requires code to be adapted to Verus-compatible syntax; Section 2.1 says nontrivial proofs often need annotations. The Introduction also documents a scarcity of Verus specifications and proofs. Our copy does not establish that ownership constraints or verbose syntax create the claimed syntax barrier. (LLM, conf=0.84)

  Experimental — accuracy not yet measured
• cites Shefer et al., 2025 sourcePartly supported

  Section 3.1 (p. 11) says Verus code generation frequently encounters type errors because of its complex type system and the different types permitted in code and invariants. The Evaluation (p. 9) also records syntax errors and notes that Verus has less training code available than Dafny. These passages support a barrier for LLM-generated Verus code, but do not establish ownership constraints or describe Verus syntax as verbose and strict. (LLM, conf=0.84)

  Experimental — accuracy not yet measured

May combine two claims.

Current multi-lingual benchmarks, such as VeriCoding, suffer from severe misalignment: they often present different problems to different tools, or specifications of various difficulties for the same problem.

“Current multi-lingual benchmarks, such as VeriCoding (Bursuc et al., 2025), suffer from severe misalignment: they often present different problems to different tools, or specifications of various difficulties for the same problem.”

• cites Bursuc et al., 2025 sourcePartly supported

  The Abstract (p. 1) reports different numbers of specifications for Dafny, Verus and Lean. The manual inspection in §4 (p. 6) finds weak or poorly translated specifications, including deviations from original tasks, which supports a concern about cross-language alignment. It does not establish that the benchmark suffers from severe misalignment or that it often presents different problems to different tools. (LLM, conf=0.84)

  Experimental — accuracy not yet measured

May combine two claims.

VeriCoding exhibits significant misalignment and specification weakness for the LIS problem.

“In contrast, VeriCoding exhibits significant misalignment and specification weakness for the same problem (Code 7, Code 8, Code 9).”

• cites Bursuc et al., 2025 sourcePartly supported

  Section 4, p. 6 reports weak specifications in roughly 9% of successful vericoding outputs and poor translations in another 15%, sometimes making the tasks different from those intended. That supports a general concern about specification weakness and misalignment, but the passages found do not establish it for the LIS problem specifically. (LLM, conf=0.82)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S1 (asserted), S3 (load-bearing), S4 (based).

Performance converges to near-zero across all paradigms for complex graph invariants.

“our”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

ALGOVERI provides the necessary unified testbed to bridge these divides, evaluating whether specialized training, generalist agentic repair, or math-inspired search methodologies yield the best performance on state-heavy algorithmic correctness.

“ALGOVERI provides the necessary unified testbed to bridge these divides, evaluating whether specialized training, generalist agentic repair, or math-inspired search methodologies yield the best perfor-mance on state-heavy algorithmic correctness.”

May combine two claims.

The verification system itself affects where models get stuck: some fail because they cannot consistently produce valid syntax, and others because they have difficulty finding the right proof steps.

“Second, the verification system itself affects where models get stuck: some fail because they cannot consistently produce valid syntax, and others because they have difficulty finding the right proof steps.”

May combine two claims.

For GPT-OSS-120B, repair curves fail to significantly outperform the pure sampling baseline, and repair often degrades performance.

“We observe that the repair curves (colored lines) fail to significantly outperform the pure sampling baseline (grey dashed line), and repair often degrades performance.”

May combine two claims.

ALGOVERI spans complex data structures, sorting and order statistics, weighted graph algorithms, fundamental DP/greedy problems, and selected math algorithms.

“It spans complex data structures (e.g., heaps, segment trees, redblack trees), sorting and order statistics, weighted graph algorithms (e.g., Bellman-Ford, Edmonds-Karp), fundamental DP/greedy problems, and selected math algorithms (e.g., Gaussian elimination).”

Probably not a substantial claim: may not pass S2 (checkable).

ALGOVERI provides a useful benchmark for distinguishing genuine reasoning progress from superficial syntactic proficiency.

“ALGOVERI provides a useful benchmark for distinguishing genuine reasoning progress from superficial syntactic proficiency.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

ALGOVERI consists of 77 problems that exceed the difficulty of standard coding interviews.

“The benchmark consists of 77 problems that exceed the difficulty of standard coding interviews.”

Classified as probably not a substantial claim. May combine two claims.

ALGOVERI provides a unified testbed to evaluate different paradigms, measuring whether specialized training or generalist reasoning yields better vericoding capability.

“ALGOV-ERI provides a unified testbed to evaluate these different paradigms, measuring whether specialized training (such as Re:Form) or generalist reasoning (such as Copra) yields better vericoding capability.”

May combine two claims.

More automated verifiers such as Dafny generally achieve higher success rates, whereas Verus and Lean require additional effort from the model, e.g., handling memory details or explicitly guiding proofs.

“more automated verifiers such as Dafny generally achieve higher success rates, whereas Verus and Lean require additional effort from the model, e.g., handling memory details or explicitly guiding proofs, making verification more challenging.”

May combine two claims.

Two failure modes are cheating (exploiting assume P or sorry) and algorithmic degeneracy (vericoding simpler versions of the requested algorithm).

“We summarize two failure modes based on analysis on the outputs: (1) Cheating, i.e., exploiting features like assume P, where P is a contradiction, or sorry to bypass verification, and (2) Algorithmic degeneracy, where models vericode simpler versions of the requested algorithm (e.g., Union-Find without path compression).”

• AssumptionRests on an assumption: The LLM-based semantic validator accurately identifies whether a compiler-verified solution implements the intended algorithm.

May combine two claims.

Frontier models can effectively leverage reasoning depth to repair complex proofs, whereas current open models saturate early during sequential refinement and benefit more from parallel sampling.

“Frontier models can effectively leverage reasoning depth to repair complex proofs, whereas current open models saturate early during sequential refinement, and benefit more from parallel sampling.”

May combine two claims.

The strongest models can reliably improve their solutions through repeated feedback, while current open models struggle to do so.

“First, the strongest models can reliably improve their solutions through repeated feedback, while current open models struggle to do so.”

May combine two claims.

ALGOVERI addresses limitations of prior benchmarks by introducing aligned formal specifications between different verification ecosystems, targeting textbook algorithmic complexity.

“ALGOVERI addresses these limitations by introducing an aligned formal specification between different verification ecosystems, targeting textbook algorithmic complexity.”

May combine two claims.

Across all languages, repair strategies fail to significantly outperform the sampling baseline, and deep repair (15 rounds) often degrades performance.

“Across all languages, repair strategies (solid lines) fail to significantly outperform the sampling baseline, and deep repair (Blue, 15 Rounds) often degrades performance.”

May combine two claims.

Models try to game for verification success but fail to follow instructions.

“Our results reveal a common phenomenon where models try to game for the verification success but fail to follow instructions.”

• AssumptionRests on an assumption: The LLM-based semantic validator accurately identifies whether a compiler-verified solution implements the intended algorithm.

May combine two claims.

In Dafny, early syntax and type mistakes are quickly fixed within the first few rounds, and most remaining errors come from failed verification checks.

“Early on, the model makes syntax and type mistakes, but these are quickly fixed within the first few rounds.After that, most remaining errors come from failed verification checks.”

May combine two claims.

For current open models, repair is inefficient and allocating budget to reasoning depth cannot exceed parallel sampling.

“Through an iso-compute analysis, we find that for current open models, repair is inefficient and allocating budget to reasoning depth cannot exceed parallel sampling (Huang et al., 2024).”

• cites Huang et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Models achieve reasonable performance on basic data structures and sorting but struggle on graph problems that involve ghost state and complex, global reasoning.

“While models achieve reasonable performance on basic data structures and sorting, they struggle on graph problems that involve ghost state and complex, global reasoning.”

May combine two claims.

With Dafny, models can usually write valid code and focus on whether the logic is correct; in Verus, they often get stuck trying to write code that parses; in Lean, they struggle to search for the right proof steps and sometimes make up tactics or lemmas.

“With Dafny, models can usually write valid code and focus on whether the logic is correct.In Verus, they often get stuck just trying to write code that parses, and in Lean they strug-gle because they have to search for the right proof steps and sometimes make up tactics or lemmas.”

May combine two claims.

Lean is dominated by a dual burden of Hallucination (Search) and Verification (Reasoning), indicating that the model struggles to simultaneously retrieve valid lemmas and apply them correctly.

“(c) Lean: Dominated by a dual burden of Hallucination (Search) and Verification (Reasoning), indicating that the model struggles to simultaneously retrieve valid lemmas (grounding) and apply them correctly.”

Probably not a substantial claim: may not pass S3 (load-bearing).

To prove the theorem in the Lean example, the model must synthesize the correct path: unfolding the function definition, extracting the property from the result subtype, simplifying the goal, and closing the goal.

“In the previous example, to prove the theorem, the model must synthesize the correct path: explicitly unfolding the function definition (→ unfold), extracting the property from the result subtype (→ let), simplifying the goal to match the extracted property (→ simp), and finally closing the goal (→ exact).”

May combine two claims.

Existing benchmarks for vericoding test only individual languages/tools (e.g., Dafny, Verus, Lean) and cover very different tasks, so their performance numbers are not directly comparable.

“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.”

Probably not a substantial claim: may not pass S4 (based).

Most existing benchmarks mainly consider tasks that do not require reasoning about global properties, which are needed in real software systems.

“Most existing benchmarks mainly consider tasks that do not require reasoning about global properties, which are needed in real software systems.”

May combine two claims.

Language design affects the refinement trajectory: Dafny allows models to focus on logical correctness, while Verus and Lean trap models in persistent syntactic and semantic barriers.

“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.”

May combine two claims.

Current LLMs often verify single operations but struggle when operations need reasoning about complex, global properties.

“While current LLMs often verify single operations, such as proving a BST rotation preserves local ordering, they struggle when the operations need reasoning about complex, global properties.”

May combine two claims.

By disentangling problem difficulty from toolchain effects, ALGOVERI revealed a clear language hierarchy: high-level SMT automation (Dafny) currently offers the most viable path for LLMs, whereas syntactic burdens of Verus and search space of Lean remain significant barriers.

“By disentangling problem difficulty from toolchain effects, we revealed a clear language hierarchy: highlevel SMT automation (Dafny) currently offers the most viable path for LLMs, whereas the syntactic burdens of systems-level verification (Verus) and the search space of interactive theorem proving (Lean) remain significant barriers.”

May combine two claims.

Lean is founded on a small, trusted kernel and offers a significantly higher standard of assurance than SMT-based systems.

“In contrast, Lean is founded on a small, trusted kernel.While currently less automated, Lean offers a significantly higher standard of assurance.”

May combine two claims.

Dafny's high pass rates trace to frequently utilized mathematical types (e.g., unbounded integers) and its managed memory model, which frees the user from expressing complex memory management logic.

“Dafny's high pass rates trace to frequently utilized mathematical types (e.g., unbounded integers) and its a managed memory model, which frees the user from expressing complex memory management logic.”

May combine two claims.

The model effectively utilizes compiler feedback to fix complex errors, treating the verifier as a constructive reward signal.

“This indicates that the model effectively utilizes compiler feedback to fix complex errors, treating the verifier as a constructive reward signal.”

Classified as probably not a substantial claim.

ALGOVERI adds a semantic filter using an LLM to assess whether a compiler verified solution matches the intended algorithm description.

“we add a semantic filter using an LLM to assess whether a compiler verified solution matches the intended algorithm description.”

• AssumptionRests on an assumption: The LLM-based semantic validator accurately identifies whether a compiler-verified solution implements the intended algorithm.

May combine two claims.

ALGOVERI mechanizes two conditions in Lean: local satisfiability and necessity against degeneracy.

“We decompose the specification into sub-clauses {C i } and mechanize two conditions in Lean: (i) Local satisfiability, proving each C i is free of internal contradictions (i.e., there exists a proof for C i ); and (ii) Necessity against degeneracy, demonstrating that dropping any C i admits unintended behaviors (e.g., dropping a permutation constraint allows an arbitrary sorted list).”

May combine two claims.

For current open models, repair is inefficient: the model might take compiler feedback as 'resampling with context' rather than a refinement process.

“This implies that for current open models, repair is inefficient: the model might take the compiler feedback as”

May combine two claims.

Verus is harder for models to work with compared to Dafny because Verus is written using Rust macros, so the model must follow both Rust's strict syntax and Verus's verification rules.

“We believe this happens because Verus is harder for models to work with compared to Dafny.Note that Verus is written using Rust macros, and therefore, the model has to follow both Rust's strict syntax and Verus's verification rules at the same time.”

The quote only partly states this claim.

Systems-level memory constraints in Verus make verification harder.

“performance collapses under the systems-level memory constraints of Verus”

Classified as probably not a substantial claim.

The primary judgment in ALGOVERI remains formal verification by compiler.

“This validator acts as a sanity check, and the primary judgment remains formal verification by compiler.”

• AssumptionRests on an assumption: The LLM-based semantic validator accurately identifies whether a compiler-verified solution implements the intended algorithm.

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

Prior works like VeriCoding have reported high success rates, with over 80% for Dafny and 40% for Verus.

“Prior works like Veri-Coding have reported high success rates, with over 80% for Dafny and 40% for Verus”

May combine two claims.

Lean is not just a search problem but a challenge of retrieval-augmented reasoning, where the model must simultaneously navigate a massive library and satisfy strict logical constraints.

“This characterizes Lean not just as a search problem, but as a challenge of retrieval-augmented reasoning, where the model must simultaneously navigate a massive library and satisfy strict logical constraints.”

May combine two claims.

The open model lacks the reasoning depth to navigate multi-turn repair chains; once simple syntax errors are resolved, it struggles to correct deeper verification failures.

“This suggests that the open model lacks the reasoning depth to navigate multiturn repair chains; once the”

Probably not a substantial claim: may not pass S3 (load-bearing).

ALGOVERI conducts well-formedness checks on representative hard tasks (e.g., Maximum Flow, Tarjan's SCC) to ensure quality of specifications.

“We also conduct wellformedness checks on representative hard tasks (e.g., Maximum Flow, Tarjan's SCC) to better ensure the quality of the specifications.”

Classified as probably not a substantial claim.

High-level abstractions and SMT automation simplify the workflow in Dafny.

“where high-level abstractions and SMT automation simplify the workflow”

May combine two claims.

By ensuring specifications are semantically aligned across languages, ALGOVERI separates problem difficulty from tool-chain effects, enabling the first true comparison of neuro-symbolic reasoning across verifiers.

“By ensuring that specifications are semantically aligned across languages, we separate problem difficulty from tool-chain effects, enabling the first true comparison of neuro-symbolic reasoning across verifiers.”

May combine two claims.

For current open models, repair is inefficient-allocating compute to depth yields no marginal gain over simple parallel sampling.

“This confirms that for current open models, repair is inefficientallocating compute to depth yields no marginal gain over simple parallel sampling.”

Classified as probably not a substantial claim.

AlgoVeri uses an LLM judge as a semantic validator to check if the generated code implements the designated algorithm after successful verification.

“If the generated code (implementation and proof) is successfully verified, an LLM judge check if the code implements the designated algorithm, serving as a semantic validator.”

Classified as probably not a substantial claim.

ALGOVERI's LIS postconditions require no longer valid subsequence exists.

“(1) there exists a valid subsequence of the returned length, and (2) no longer valid subsequence exists.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Interactive theorem proving in Lean presents a search barrier, where the model acts as an agent navigating a state space.

“This presents a search barrier.Besides fighting syntax, the model acts as an agent navigating a state space.”

May combine two claims.

ALGOVERI's benchmark design has two key principles: strict alignment across languages and algorithmic rigor.

“These codes demonstrate the two key principles of our benchmark design: strict alignment across languages and algorithmic rigor.”

Probably not a substantial claim: may not pass S3 (load-bearing).

A failure in the Lean proof search is a navigation error-choosing a tactic that leads to an unsolvable state.

“A failure here is a navigation error-choosing a tactic that leads to an unsolvable state.”

Probably not a substantial claim: may not pass S3 (load-bearing).

ALGOVERI's Max Flow specifications require models to reason about global graph invariants and existential witnesses for optimality.

“This example illustrates the depth of our specifications, which require models to reason about global graph invariants and existential witnesses for optimality.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The Max Flow problem requires rigorous graph-theoretic modeling within the specification logic.

“Representing the high-complexity tier of our benchmark, the Max Flow problem requires rigorous graph-theoretic modeling within the specification logic.”

Probably not a substantial claim: may not pass S4 (based).

The LLM may write a set of First-order logic (FOL) formulas in ghost proofs whose conjunction may fall outside the decidable fragment (e.g., EPR) of FOL.

“For example, the LLM may write a set of First-order logic (FOL) formulas in ghost proofs, whose conjunction may fall outside the decidable fragment (e.g., EPR) of FOL.”

• AssumptionRests on an assumption: Deciding the satisfiability of the proof artifact can be undecidable.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

For an LLM, type errors in verification-aware type systems are 'syntax-plus' barriers.

“For an LLM, these are”

• AssumptionRests on an assumption: In program verification, a type error represents a failure to satisfy the rigid structural rules enforced by the language's type system before verification even begins.
• AssumptionRests on an assumption: Verification-aware type systems might include stricter rules than standard compilation.

Classified as probably not a substantial claim.

ALGOVERI's Max Flow specifications define global invariants such as flow conservation, capacity constraints, and global optimality (is_max_flow).

“Unlike simpler algorithmic tasks, the specifications here must define global invariants such as flow conservation, capacity constraints, and global optimality (is_max_flow).”

May combine two claims.

The difficulty in SMT-based verification lies in encoding abstract reasoning into the system's rigid syntax, and this is particularly pronounced in Verus.

“The difficulty lies in encoding abstract reasoning into the system's rigid syntax.This is particularly pronounced in Verus, where the model must bridge the gap between low-level system types and mathematical logic.”

• AssumptionRests on an assumption: Dafny natively supports mathematical types.
• AssumptionRests on an assumption: Verus verifies Rust, a systems language.
• AssumptionRests on an assumption: Both Dafny and Verus use SMT-based verification.

Classified as probably not a substantial claim.

ALGOVERI's Max Flow postcondition requires an existential witness.

“Crucially, the postcondition demands more than just a correct return value; it requires an existential witness.”

Classified as probably not a substantial claim.

ALGOVERI's LIS postconditions require there exists a valid subsequence of the returned length.

“(1) there exists a valid subsequence of the returned length, and (2) no longer valid subsequence exists.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The Max Flow problem represents the high-complexity tier of ALGOVERI.

“Representing the high-complexity tier of our benchmark, the Max Flow problem requires rigorous graph-theoretic modeling within the specification logic.”

Classified as probably not a substantial claim.

ALGOVERI's Max Flow postcondition demands more than just a correct return value.

“Crucially, the postcondition demands more than just a correct return value; it requires an existential witness.”

Classified as probably not a substantial claim. May combine two claims.

In such a case, the decision procedure of SMT solvers may diverge (infinite-loop) or output unknown, which is inconclusive for the verification results.

“In such a case, the decision procedure of SMT solvers may diverge (infinite-loop) or output unknown, which is inconclusive for the verification results.”

• AssumptionRests on an assumption: Deciding the satisfiability of the proof artifact can be undecidable.