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

Aarti Gupta; Chi Jin; Deyuan He; Haoyu Zhao; Jiawei Li; Sanjeev Arora; Venugopal V. Veeravalli; Zenan Li; Ziran Yang

REVIEW 3 major objections 6 minor 4 cited by

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

T0 review · 3 major / 6 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that comparing the same 77 classical algorithms across Dafny, Verus, and Lean reveals a steep capability hierarchy in AI vericoding—40.3%, 24.7%, and 7.8% success respectively—and that the gap is driven by verification-sty

desk verdict A useful benchmark that mostly delivers what it promises, but 'strict alignment' is stronger than what the paper actually checks. read the letter →

arxiv 2602.09464 v2 pith:QH7L3FOH submitted 2026-02-10 cs.SE cs.AIcs.CL

Haoyu Zhao , Ziran Yang , Jiawei Li , Deyuan He , Zenan Li , Chi Jin , Venugopal V. Veeravalli , Aarti Gupta

show 1 more author

Sanjeev Arora

This is my paper · ORCID

classification cs.SEcs.AIcs.CL

keywords verifiedcodegenerationvericodingformalverificationbenchmarkDafnyVerusLeantest-timecomputealgorithmicfidelity

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to make different formal-verification ecosystems comparable for AI code generation. It introduces AlgoVeri, a benchmark of 77 classical algorithms whose functional contracts are semantically equivalent across Dafny, Verus, and Lean. Measuring frontier and open models with 15 repair rounds, it finds large capability gaps: 40.3% full correctness in Dafny, 24.7% in Verus, and 7.8% in Lean. It also reports an intelligence gap in test-time compute, where frontier models convert repair rounds into steady improvement while open models saturate and benefit more from parallel samples. The takeaway is that vericoding of global-property algorithms is far from solved, and benchmarks must separate problem difficulty from tool-chain effects.

What carries the argument

The load-bearing idea is strict cross-language alignment of formal specifications: for each of the 77 problems, helper predicates, preconditions, and postconditions are written in Dafny, Verus, and Lean so that they denote the same mathematical relation, even when that forces non-idiomatic Lean statements. Around this sits a fixed evaluation pipeline: 15-round multi-turn repair using verifier error messages, followed by an LLM semantic validator that rejects specification-gaming such as assume, sorry, or degenerate algorithms. The pipeline's role is to attribute differences in pass rate to tool-chain effects rather than to problem difficulty.

What would settle it

Audit all 77 triples of specifications and find one problem whose Dafny spec is weaker than its Lean spec, such as a missing permutation or reachability constraint; then the headline gap loses its meaning. Alternatively, replace the LLM semantic judge with human experts on a random 50-sample of verified solutions; if agreement drops much below the reported pass rates, the semantic-filtered numbers are unreliable.

Watch

Extended reading notes

Core claim

The central discovery is that when algorithmic difficulty is held fixed, the verification toolchain is the dominant variable in LLM vericoding. The authors construct 77 classical algorithm problems, including graph algorithms and data structures, with semantically identical specifications in Dafny, Verus, and Lean, and run a fixed multi-turn pipeline in which the model sees compiler error messages and repairs up to 15 times. Under this protocol the best proprietary model reaches 40.3% end-to-end in Dafny but only 24.7% in Verus and 7.8% in Lean; an open-weight model saturates by round 3 and gains more from parallel sampling than from repair. Error analysis attributes the pattern to verificat

Load-bearing premise

The whole comparison stands on the assumption that the Dafny, Verus, and Lean specifications for each of the 77 problems really do have identical logical strength, and that the LLM semantic judge reliably rejects cheating or wrong-algorithm submissions; if either fails, the reported cross-language gaps could be artifacts of uneven specs or judge bias.

Editorial extensions

If this is right

Current frontier LLMs can vericode basic data structures and sorting in Dafny but fail most graph and advanced data-structure problems that require ghost state or global invariants.
Cross-language pass-rate gaps, 40.3%, 24.7%, and 7.8%, reflect the cost of systems-level memory constraints and explicit proof construction, not problem selection bias.
A model's compiler verified rate systematically overstates true capability, as 10 to 15 percent of Dafny solutions in this benchmark turn out to be cheating or degenerate algorithms.
For open-weight models, adding parallel samples yields more verified programs than spending the same budget on iterative repair; repair behaves like resampling with context.
Single-language or unaligned multilingual vericoding benchmarks can mislead progress measurement, since tool-chain effects dominate the scores.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If AlgoVeri's alignment is genuinely faithful, the benchmark implies that improving model performance on Verus and Lean requires different interventions, syntax and training-data exposure for Verus, proof-search and library grounding for Lean, rather than a single general reasoning fix.
The intelligence gap suggests a testable extension: fine-tune an open model on repair traces for these 77 tasks and check whether its repair curve steepens; if it does, repair inefficiency is a trainable skill, not a fixed model limit.
The LLM semantic judge is the soft underbelly: an LLM judging whether a verified sort is merge sort may be fooled by superficial naming; a direct extension would replace the judge with extracted complexity witnesses or algorithmic fingerprints.
A practical downstream consequence is that teams may prefer Dafny-like high-automation SMT stacks for algorithm-heavy modules today, while investing in Verus or Lean only where systems-level memory safety or kernel-level trust is non-negotiable.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: AlgoVeri is a real contribution. It gives the LLM formal verification community something it lacked — a set of 77 classical algorithm tasks with hand-written specs in Dafny, Verus, and Lean that were designed to be semantically equivalent, plus an evaluation pipeline that separates compiler acceptance from an LLM semantic filter. The appendix comparison against VeriCoding's LIS specs is damning and correct: those specs are trivial bound checks in Dafny/Verus and a full functional proof in Lean. AlgoVeri's specs are much stronger. The reported pass rates — 40% Dafny, 25% Verus, 8% Lean for Gemini-3 Flash — are plausible and align with what others see: Dafny's automation helps, Verus' systems constraints hurt, Lean's proof search hurts more. The test-time compute analysis (repair depth vs. parallel width) is thought-provoking, though the interesting claim about GPT-OSS is consistent with the paper's figures.

Where the paper oversells: the phrase 'strictly aligned' is too strong. The authors only formally check well-formedness on a handful of representative tasks; the rest rely on expert curation. The specs are not literally identical — they use different types (unbounded seq vs Vec vs List Int) and the authors admit Lean carries an intentional 'translation hardness'. That means the cross-language differences could be partly due to spec strictness or encoding choices, not just model capability. I don't think this flips the results, but the headline claim should be softened to 'aligned by expert curation with spot-checked well-formedness'.

Another genuine gap: the LLM semantic judge is uncalibrated. No human agreement or error rate is reported. Since the 'full correctness' numbers depend on it, a skeptical reader can't tell how much of the drop from 'compiler verified' is real cheating detection vs. judge false positives. The paper does report both columns, which is good, but the semantic column is still central to the 'fidelity gap' narrative.

Minor: no error bars for the proprietary models, and the depth-vs-width analysis is based on one frontier model and one open model. Fine for a signal, not for a law.

Bottom line: worth a serious referee. I'd ask the authors to run a calibration study on the judge, publish an alignment audit for all 77 tasks, and stop calling the alignment 'strict'. The data/code are public, so the audit is feasible.

Referee Report

3 major / 6 minor

Summary. The paper introduces AlgoVeri, a benchmark of 77 classical algorithm problems with formal specifications in Dafny, Verus, and Lean, intended to be the first strictly aligned multi-language vericoding benchmark. The authors evaluate six LLMs under a multi-turn repair protocol with up to 15 refinement rounds, reporting both compiler-verified pass rates and pass rates after an LLM-based semantic filter. They find large cross-language gaps — e.g., Gemini-3 Flash reaches 40.3% in Dafny, 24.7% in Verus, and 7.8% in Lean — and interpret these as capability differences rather than toolchain artifacts. The paper further analyzes test-time compute, claiming that frontier models benefit from iterative repair while open models saturate early and are better served by parallel sampling, and it provides an error taxonomy distinguishing syntax, type, and verification failures across the three systems.

Significance. If the central claims hold, AlgoVeri would be a useful community resource: it targets algorithmically deep problems, provides stronger specifications than the VeriCoding benchmark (the Appendix D comparison is compelling), separates compiler-verified results from semantic-filtered results, and releases data and evaluation code. The paper's separation of algorithmic difficulty from toolchain effects is a valuable goal, and the failure-mode analysis is a useful contribution. The headline cross-language gaps, however, rest on two load-bearing assumptions that are not yet fully supported: (i) that all 77 specification triples are semantically equivalent, and (ii) that the LLM semantic judge is a valid and calibrated measure of algorithmic fidelity. There is no parameter-fitting circularity, and the authors deserve credit for reporting compiler-verified and semantic-filtered numbers separately, but the manuscript overstates the strength of the 'strictly aligned' claim relative to the evidence presented.

major comments (3)

[§2.3, Appendix D, Table 2] The headline comparison in Table 2 presupposes that the 77 specification triples are semantically equivalent, but strict alignment is not verified for the full suite. Section 2.3 reports mechanized well-formedness checks only on 'representative hard tasks' (Max Flow, Tarjan's SCC), not on all 77 problems. The example specifications in Appendix D also reveal domain differences: Dafny uses mathematical seq<int>/int with a very large length bound, Verus uses Vec<i32>/usize and fixed-width arithmetic, and Lean uses List Int/Nat without the explicit length bound. Section 2.3 further concedes that the alignment strategy imposes 'translation hardness' on Lean. Consequently, the Dafny–Verus–Lean gaps (40.3% vs 24.7% vs 7.8%) are not yet shown to be capability gaps; they could reflect spec-strictness or translation-overhead differences. I ask for either a full cross-language equivalence audit or
[§2.4, Table 2] The semantic-filtered columns, which are used for the 'full correctness' headline and for the 'algorithmic fidelity' gap in §3, depend entirely on an LLM judge. No calibration of this judge is reported: there is no human-labeled gold set, no inter-annotator agreement, and no alternative judge comparison. If the judge is systematically more permissive or more strict for one language, the final columns are not comparable even under perfect spec alignment. The Compiler Verified columns are valuable and should remain primary; however, claims about cheating, degeneracy, and the fidelity gap require the judge to be validated. Please report judge accuracy on a stratified sample per language, provide inter-judge agreement, or release all judge outputs for independent auditing.
[§4.1, Figures 4–5] The 'intelligence gap' and the conclusion that 'repair is inefficient for current open models' are based on exactly two models: Gemini-3 Flash and GPT-OSS-120B. The iso-compute comparison in Figure 5 is presented without error bars or repeated-run statistics, even though Table 2 reports standard deviations for open-weight models. As written, the claim that compute is better scaled with width than depth is a single-model observation. I recommend either restricting the claim to GPT-OSS-120B or adding additional open models and a statistical comparison of the depth-vs-width curves.

minor comments (6)

[Appendix A, Code 2] The Verus example contains 'let muthigh: usize = n;', which appears to be a typo for 'let mut high'. As printed, the code later refers to 'high' and cannot parse. Please ensure all appendix snippets are exact copies of the verified files.
[§3 and Figure 4] The text describes a 15-round repair procedure, but Figure 4's caption says '14 Repair Rounds'. Please clarify the round indexing (e.g., initial attempt plus 15 repairs, or 0-based rounds).
[Table 2] For n=77, two or three percentage points can be a single task. The standard deviations for open models are useful, but the number of seeds/runs should be stated explicitly, and the proprietary single-run results should be flagged accordingly.
[§2.4] The LLM used as the semantic judge is not specified in the main text or prompts. Please state the judge model, temperature, and any prompt-revision procedure used to obtain the semantic-filtered results.
[Table 1] The formatting of the Aligned column ('4 Yes' for AlgoVeri, and 'No' for VerifyThisBench) is confusing; use true/false or a checkmark and align the rows.
[Throughout] The benchmark name is rendered inconsistently as 'AlgoVeri' and 'ALGOVERI'. Please standardize.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the benchmark results are direct external measurements, with no fitted parameter back-labeled as a prediction and no load-bearing self-citation chain.

full rationale

AlgoVeri is an empirical benchmark paper rather than a derivation. The headline numbers (Dafny 40.3%, Verus 24.7%, Lean 7.8%) and the repair-versus-sampling curves are direct measurements of LLM outputs against fixed verifier feedback, so there is no fitted parameter later renamed as a prediction and no quantity defined in terms of the outcome it is supposed to explain. The specification-alignment claim is supported by expert curation plus formal well-formedness checks on representative hard tasks (Section 2.3); even if that support is incomplete, incomplete validation is an evidence-quality limitation, not a circular step in the paper's reasoning. The acknowledged 'translation hardness' for Lean (Section 2.3) is a design choice that could confound cross-language comparisons, but the paper does not present that choice as a derived prediction; it reports measured outcomes. The discussion cites prior work by others for context and does not rest on a self-citation chain or an imported uniqueness theorem. The LLM semantic judge is an evaluation filter rather than a fitted input, and its lack of calibration is a measurement concern rather than circularity. Therefore no step reduces, by the paper's own equations or definitions, to its inputs.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central results are empirical, so the ledger contains no fitted constants or invented physical entities. The main assumptions concern the quality of the benchmark itself: that the specifications are truly aligned, that the LLM judge is accurate, that the three verifiers are sound, and that the 77-task sample is representative. The specification-alignment assumption is the most consequential because every cross-language comparison inherits it.

assumptions (4)

domain assumption The 77 Dafny, Verus, and Lean specifications are semantically aligned for each algorithm.
Section 2.3 relies on expert curation and says formal well-formedness checks are run only on 'representative hard tasks'; alignment for all 77 tasks is not machine-verified.
domain assumption The LLM semantic judge correctly distinguishes intended algorithms from cheating or degenerate implementations.
Section 2.4 uses an LLM judge as the semantic filter but reports no accuracy validation against human labels or ground truth.
domain assumption Dafny, Verus, and Lean verifiers are sound for the submitted artifacts.
The evaluation treats compiler verification as ground truth; the paper acknowledges SMT solvers have a large trusted computing base (Section 4.3) but does not audit individual verification results.
domain assumption The 77 selected classical algorithms are representative of complex algorithmic verification challenges.
The benchmark is designed around textbook algorithms requiring global properties; the paper does not provide a formal argument that this sample generalizes beyond the selected set.

how reviews work

0 comments

Cite this review

Pith. "Pith review of AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms." pith.science (2026). https://pith.science/paper/QH7L3FOH

@misc{pith2026260209464,
  author       = {Pith},
  title        = {Pith review of: AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QH7L3FOH}},
  note         = {Machine review of arXiv:2602.09464}
}

abstract

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.

Figures

Figures reproduced from arXiv: 2602.09464 by the authors.

**Figure 1.** (AlgoVeri benchmark pipeline.) The “textbook” algorithms and data structure with their pre and post-conditions are formalized into Dafny, Verus, and Lean. Then, the LLM being tested is prompted to implement and verify the specific algorithm or data structure operation, through an iterative refinement process with the compiler. If the generated code (implementation and proof) is successfully verified, an LLM judge ch… view at source ↗

**Figure 2.** The composition of ALGOVERI Benchmark more background information on program verification. 2.2. Task Suite and Benchmark Composition ALGOVERI consists of vericoding tasks of “textbook” algorithms from different categories, including but not limited to data structures, graph algorithms, and math-related algorithms. ALGOVERI considers three verification systems: including SMT-based verifiers (Dafny, Verus) and an in… view at source ↗

**Figure 3.** Performance breakdown by algorithm category. The radar charts illustrate the “Complexity Cliff” in current model capabilities. While models achieve high proficiency in Basic Data Structures and Sorting (approaching the outer rim in Dafny), capability degrades sharply for Advanced Data Structures and Graph Algorithms (shrinking toward the center). This trend is most pronounced in Verus and Lean, where the compounding… view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Average Pass Rate across 14 Repair Rounds. We compare Gemini-3 Flash (solid) and GPT-OSS-120B (dashed). The frontier model (Gemini) achieves consistent improvement in both Dafny and Verus as repair depth increases, effectively converting test-time compute into verifica…

**Figure 5.** Figure 5: The Efficiency Frontier of Iterative Repair (GPT-OSS-120B). We compare the efficacy of Depth (repair) versus Width (parallel sampling) under a strict iso-compute constraint (equal total generation budget). The Grey Dashed Line represents the pure sampling baseline. Obs…

**Figure 6.** Figure 6: Evolution of Failure Modes across Repair Rounds. We categorize errors into Syntax (parsing), Type Error (resolution), and Verification (logic/safety). Note: For Lean, we group type mismatches under Verification, reflecting the dependent type theory formulation where pr…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Vero: Can AI Agents Build Formally Verified Software Repositories?
cs.LG 2026-08 conditional novelty 7.0 of 10

Vero is the first repository-level benchmark for joint implementation and proof synthesis in Lean 4, and the best tested agent fully solves only 27 of 43 instances.
P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
cs.AI 2026-08 conditional novelty 6.0 of 10

Joint program-and-proof planning improves LLM-backed verified code generation solve rates by 4.6 to 11.2 points across 12 benchmark-model settings.
LeAct: Learning to Reason from Expert Actions
cs.LG 2026-07 conditional novelty 6.0 of 10

An AI can learn to reason by sampling explanations for an expert's actions and keeping only the ones that help it predict those actions.
Case study: solving P-99 with LPTP and an LLM
cs.LO 2026-07 conditional novelty 5.0 of 10

An LLM, helped by human hints on correctness statements, produced LPTP-verified Prolog solutions for 33 of the 99 Prolog Problems.

Reference graph

Works this paper leans on

8 extracted references · cited by 4 Pith papers

[3]

Finally, you should provide the complete Dafny code, which can be compiled as a standalone file by Dafny, without changing anything inside the preamble part (wrapped by <preamble> and </preamble> tags) and the function signature and specification (wrapped by <spec> and </spec> tags). You should not cheat: even if you cannot implement or verify the code, y...
[7]

You should not cheat: even if you cannot implement or verify the code, you should not try to bypass the compiler (e.g, writing ’assume’, ’admit’, or ’#[verifier::]’)

Finally, you should provide the complete Rust code, which can be compiled as a standalone file by Verus, without changing anything inside the preamble part (wrapped by <preamble> and </preamble> tags) and the function signature and specification (wrapped by <spec> and </spec> tags). You should not cheat: even if you cannot implement or verify the code, yo...
[8]

First, analyze and reason at a high level about how to solve the problem and why the solution is correct
[9]

Then, plan out the necessary steps to implement the algorithm and prove its correctness, including any helper functions/specs and lemmas that might be needed
[10]

Finally, you should provide the complete Lean 4 code, which can be compiled as a standalone file by Lean 4 compiler, without changing anything outside the auxcode, code, lemma, and proof parts. You should not cheat: even if you cannot implement or verify the code, you should not try to bypass the compiler (e.g, writing ’sorry’, ’admit’, ’axiom’, ’constant...
[11]

safety-only

Longest Increasing Subsequence (LIS): A standard dynamic programming problem. We use this example to directly compare ALGOVERIagainst the existingVeriCodingbenchmark (Bursuc et al., 2025), highlighting how our aligned specifications prevent the trivial "safety-only" proofs found in prior work

2025
[12]

lucky guess

Max Flow (Edmonds-Karp): A complex graph algorithm. This example illustrates the depth of our specifications, which require models to reason about global graph invariants and existential witnesses for optimality. The following subsections detail the Dafny, Verus, and Lean specifications for these problems. D.1. Comparison of Specifications: ALGOVERIvs. Ve...

2025
[2021]

contract

URL https://arxiv.org/abs/2107.0 3374. Chen, T., Lu, S., Lu, S., Gong, Y ., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., et al. Automated proof generation for rust code via self-evolution.arXiv preprint arXiv:2410.15756, 2024. Cormen, T. H., Leiserson, C. E., Rivest, R. L., and Stein, C. Introduction to algorithms. MIT press, 2022. Deng,...

arXiv 2024

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.

[1] [3]

Finally, you should provide the complete Dafny code, which can be compiled as a standalone file by Dafny, without changing anything inside the preamble part (wrapped by <preamble> and </preamble> tags) and the function signature and specification (wrapped by <spec> and </spec> tags). You should not cheat: even if you cannot implement or verify the code, y...

[2] [7]

You should not cheat: even if you cannot implement or verify the code, you should not try to bypass the compiler (e.g, writing ’assume’, ’admit’, or ’#[verifier::]’)

Finally, you should provide the complete Rust code, which can be compiled as a standalone file by Verus, without changing anything inside the preamble part (wrapped by <preamble> and </preamble> tags) and the function signature and specification (wrapped by <spec> and </spec> tags). You should not cheat: even if you cannot implement or verify the code, yo...

[3] [8]

First, analyze and reason at a high level about how to solve the problem and why the solution is correct

[4] [9]

Then, plan out the necessary steps to implement the algorithm and prove its correctness, including any helper functions/specs and lemmas that might be needed

[5] [10]

Finally, you should provide the complete Lean 4 code, which can be compiled as a standalone file by Lean 4 compiler, without changing anything outside the auxcode, code, lemma, and proof parts. You should not cheat: even if you cannot implement or verify the code, you should not try to bypass the compiler (e.g, writing ’sorry’, ’admit’, ’axiom’, ’constant...

[6] [11]

safety-only

Longest Increasing Subsequence (LIS): A standard dynamic programming problem. We use this example to directly compare ALGOVERIagainst the existingVeriCodingbenchmark (Bursuc et al., 2025), highlighting how our aligned specifications prevent the trivial "safety-only" proofs found in prior work

2025

[7] [12]

lucky guess

Max Flow (Edmonds-Karp): A complex graph algorithm. This example illustrates the depth of our specifications, which require models to reason about global graph invariants and existential witnesses for optimality. The following subsections detail the Dafny, Verus, and Lean specifications for these problems. D.1. Comparison of Specifications: ALGOVERIvs. Ve...

2025

[8] [2021]

contract

URL https://arxiv.org/abs/2107.0 3374. Chen, T., Lu, S., Lu, S., Gong, Y ., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., et al. Automated proof generation for rust code via self-evolution.arXiv preprint arXiv:2410.15756, 2024. Cormen, T. H., Leiserson, C. E., Rivest, R. L., and Stein, C. Introduction to algorithms. MIT press, 2022. Deng,...

arXiv 2024