{"id":"e225ade8-105c-4e67-a74c-90d5fe678c36","arxiv_id":"2602.09464","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"AlgoVeri introduces the first aligned three-language benchmark for verified code generation and reports that current models reach 40.3% (Dafny), 24.7% (Verus), and 7.8% (Lean) full correctness.","lead":"AlgoVeri is a benchmark of 77 classical algorithms, each with matching formal specifications in Dafny, Verus, and Lean, used to test how well AI models generate provably correct code. In tests, the best model passed 40.3% of tasks in Dafny but under 8% in Lean, showing verified-code generation is far from solved.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Strict alignment of all 77 specs is asserted but formally checked only on representative tasks; without a full equivalence audit, cross-language gaps could reflect spec-strictness differences.","rationale":"The reader's weakest assumption is precisely the semantic alignment of all 77 specifications plus the reliability of the LLM judge. I agree with that diagnosis, and I would single out the alignment leg as the more load-bearing of the two: if the specs are not equivalent, the central comparison collapses regardless of judge quality. The paper's own text supports the concern rather than dispelling it: formal checks are explicitly limited to representative hard tasks, and the authors acknowledge that the alignment strategy imposes translation hardness on Lean. This does not prove the claim false, but it leaves the key premise validated only by human curation and two examples. The LLM judge compounds the issue because the headline numbers are semantic-filtered, and no calibration against expert labels is reported. A full formal equivalence audit and degenerate-implementation battery would settle whether the alignment claim holds. Since the concern is about missing validation rather than demonstrated inconsistency, the verdict should remain conditional rather than move to accept or reject.","tokens_in":26860,"tokens_out":10226,"duration_ms":108524,"concrete_test":"Audit all 77 tasks, not just Max Flow and Tarjan's SCC: for each task, translate the Dafny, Verus, and Lean contracts into a common logical representation and prove pairwise semantic equivalence under the intended algorithm semantics. In the same audit, run a small fixed battery of degenerate/reference implementations (return constant, trivial algorithm, assume False/sorry, correct reference) through all three verifiers and confirm identical acceptance patterns. Any divergence in acceptance behavior would falsify the strict-alignment premise.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is not just that models fail at verified code generation, but that AlgoVeri is strictly aligned and therefore separates problem difficulty from tool-chain effects. That separation is load-bearing: the headline gaps (Dafny 40.3%, Verus 24.7%, Lean 7.8%) are only meaningful if the 77 spec triples are semantically equivalent. Section 2.3 limits formal well-formedness checks to 'representative hard tasks' (Max Flow, Tarjan's SCC), leaving the remaining tasks to expert curation. No cross-language equivalence proof is reported for the full suite. Appendix D shows the contracts are not literally identical: Dafny uses unbounded seq<int>/int, Verus uses Vec<i32>/u64 with an explicit length bound, and Lean uses List Int/Nat without that bound. Section 2.3 also concedes the alignment strategy may impose 'translation hardness' on Lean. If any contracts differ in strictness or domain, the observed rate differences could be artifacts of specification strictness or translation overhead rather than model capability. The LLM semantic judge, used for the headline 'full correctness' numbers, is also reported without accuracy calibration; but even a perfect judge would not resolve the alignment question.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":27063,"tokens_out":6800,"duration_ms":73383,"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":[{"comment":"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","section":"§2.3, Appendix D, Table 2"},{"comment":"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.","section":"§2.4, Table 2"},{"comment":"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.","section":"§4.1, Figures 4–5"}],"minor_comments":[{"comment":"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.","section":"Appendix A, Code 2"},{"comment":"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).","section":"§3 and Figure 4"},{"comment":"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.","section":"Table 2"},{"comment":"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.","section":"§2.4"},{"comment":"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.","section":"Table 1"},{"comment":"The benchmark name is rendered inconsistently as 'AlgoVeri' and 'ALGOVERI'. Please standardize.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper has a potentially strong contribution, and the fixes I am requesting are within the scope of a benchmark paper: a full or sufficiently comprehensive specification-equivalence audit, calibration of the semantic judge, and error-bar-aware depth-vs-width analysis. I do not see a load-bearing error that requires rejection, but the 'strictly aligned' claim currently outruns the evidence and should be softened or substantiated before acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhere 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<i32> 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'.\n\nAnother 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.\n\nMinor: 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.\n\nBottom 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.","headline":"A useful benchmark that mostly delivers what it promises, but 'strict alignment' is stronger than what the paper actually checks.","tokens_in":27616,"tokens_out":2682,"would_cite":true,"duration_ms":26372,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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","keywords":["verified code generation","vericoding","formal verification benchmark","Dafny","Verus","Lean","test-time compute","algorithmic fidelity"],"falsifier":"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.","tokens_in":1454,"feed_emoji":"✅","tokens_out":4428,"duration_ms":80997,"temperature":0.7,"pith_summary":"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.","feed_headline":"Same algorithms: 40% in Dafny, 8% in Lean","feed_subtitle":"Identical tasks show Dafny's automation helps frontier models, while Verus syntax and Lean proof search block most attempts.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Toolchain, not algorithm, decides AI code verification","Dafny 40% vs Lean 8%: same tasks, different ceilings","Same specs, same algorithms: LLMs flop in Lean","Why AI code proof fails: it's the language, not the logic"],"cache_read_input_tokens":28928,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Toolchain, not algorithm, decides AI code verification","Dafny 40% vs Lean 8%: same tasks, different ceilings","Same specs, same algorithms: LLMs flop in Lean","Why AI code proof fails: it's the language, not the logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00083,"raw_usage":{"total_tokens":3499,"prompt_tokens":820,"completion_tokens":2679,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":564,"completion_tokens_details":{"reasoning_tokens":2603}},"tokens_in":564,"tokens_out":2679,"duration_ms":17167,"temperature":1.0,"reasoning_tokens":2603,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T02:46:20.236962+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}