CoChat
Sign Up
PreprintCited by 2Logic, programming, and type systemsSoftware Engineering ResearchTeaching and Learning Programming

A benchmark for vericoding: formally verified program synthesis

Open access
Bursuc, Sergiu, Ehrenborg, Theodore, Lin, Shaowei, Astefanoaei, Lacramioara, Chiosa, Ionel Emilian, Kukovec, Jure, Singh, Alok, Butterley, Oliver +5 more·2025·arXiv
DOI 10.48550/arxiv.2509.22908arXiv 2509.22908
Open this paper in CoChat — free account

Abstract

We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark

AI snapshot

Written from the paper’s full text.

TL;DR

The authors introduce vericoding — LLM generation of formally verified code from formal specifications — and release the largest such benchmark to date, with 12,504 formal specifications across Dafny, Verus/Rust, and Lean. Off-the-shelf LLMs solve 82% of Dafny tasks but only 44% of Verus and 27% of Lean tasks, and adding natural-language descriptions does not significantly improve performance.

Key findings

  • The benchmark contains 12,504 formal specifications (3,029 Dafny, 2,334 Verus/Rust, 7,141 Lean), of which 6,174 are new unseen problems.
  • Vericoding success rates with off-the-shelf LLMs: 82.2% Dafny, 44.3% Verus/Rust, 26.8% Lean (model-union figures). Claude-Opus-4.1 excelled at Dafny, while GPT-5 led on Verus and Lean.
  • On the novel Numpy-Triple (Hoare triples in Lean using the new mvcgen feature), the model union achieved only 7.6%, below the Lean language average of 26.8%.
  • Pure Dafny verification (original DafnyBench, 782 tasks) improved from 68% (Opus-3, June 2024 SOTA) to 89% with Opus-4.1 and 96% for the model union.
  • Including informal "vibe" descriptions in the prompt provided no statistically significant improvement (results slightly worse on average).
  • Manual inspection of 5 successful outputs per language/source found that, conditioned on vericoding success, roughly 9% of specs were too weak and another 15% had poor translations.

Methods

  • Benchmark construction: curated original sources (DafnyBench, VerifiedCogen, Verina, Clever, APPS, FVAPPS, HumanEval, NumPy docs, BigNum), removed implementations/proofs and replaced them with holes (e.g., `sorry`), then translated specifications between Dafny, Verus, and Lean using an LLM-based translation algorithm with a conversational repair loop (up to k iterations).
  • Validation used "LLM as a judge" plus manual inspection of a random sample; quality scoring penalized language-specific issues and near-duplicates (sentence transformers + FAISS).
  • Vericoding experiments: prompts annotated with context, spec, and holes; generated blocks validated for cheating patterns (e.g., `assume(false)`, `sorry`, altered postconditions) and verified with the proof checker; errors fed back for correction. Each LLM had 5 attempts per task (10 for BigNum). 55,397 vericoding experiments were run in total.

Limitations

  • The paper states prompts were only informally explored and not fully optimized, and that the Verus prompt might benefit from examples of common vstd lemmas; the Lean prompt might benefit from examples of new tactics such as `grind` and `canonical`.
  • The paper acknowledges implementation leakage from specs is typically present to some degree, and that some specs admitted trivial solutions due to lossy LLM transpilation or incomplete human-authored specs; it also notes high near-duplicate rates for BigNum (by design) and that some NumPy specs "slipped past" hand-checking.
  • Manual inspection was limited to 5 randomly chosen successful outputs per language and data source, so cheating detection is not exhaustive.
  • Evident from the text: tasks are typically solvable in under 100 lines of code, and the benchmark covers only Dafny, Verus, and Lean; the authors note extending to more complex benchmarks like SWE-bench or BashBench remains future work.

Model-written summary. Check it against the paper before relying on it.

Integrity signals

Registry

DataCite · 10.48550/arxiv.2509.22908

Cites

29 of 29 references verified0 citation errors · 0 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

2 of 9 cited sources checked · 1 supported · 0 flagged · accuracy not yet measured

  • Premisecitation
    § 1 INTRODUCTION · p. 1

    AI tools improved their success rate from 21% to over 82% on the MetaMath benchmark over the last few years.

    “Fueled by the advent of benchmarks totaling over 100,000 theorems, AI tools have during the last few years improved their success rate from 21% to over 82% on the MetaMath benchmark (Polu & Sutskever, 2020; Lample et al., 2022).”
    Quote in the paperSubstantial claim1 of 2 sources checked
    • cites Polu & Sutskever, 2020 source

      Table 13 (A Key Results, p. 18) reports a 21.16% MetaGen-IL baseline and improvement to 56.50% for the authors’ best listed model, supporting an increase in success rate but not the claimed figure of over 82%. Section 3.2 (p. 4) describes approximately 38,000 theorems in this paper’s dataset, not over 100,000. (LLM, conf=0.90)

      Experimental — accuracy not yet measured
    • cites Lample et al., 2022

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

  • Findingown data
    § ABSTRACT · p. 1

    Of the benchmark's specifications, 6,174 are new unseen problems.

    “Of these, 6,174 are new unseen problems.”
    • Also stated in: § 3 BENCHMARK CONSTRUCTION · p. 3 · plain
      “In comparison, we have 12504 tasks of which 6174 are new or translated from other benchmarks.”
    Quote in the paperSubstantial claim
  • Findingown data
    § ABSTRACT · p. 1

    Vericoding success rate in Dafny is 82% using off-the-shelf LLMs.

    “We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs.”
    • Also stated in: § 4.1 VERICODING RESULTS · p. 7 · plain
      “Table 3 shows that LLM vericoding worked best on Dafny (82.2%), followed by Verus (44.2%) and Lean (26.8%).”
    Quote in the paperSubstantial claim
    • The authors state this as an assumption: AI will soon be able to greatly facilitate formal verification and vericoding, dramatically reducing the cost of creating bug-free software.
  • Findingown data
    § ABSTRACT · p. 1

    The benchmark contains 12,504 formal specifications.

    “Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean.”
    • Also stated in: § 3 BENCHMARK CONSTRUCTION · p. 3 · plain
      “In comparison, we have 12504 tasks of which 6174 are new or translated from other benchmarks.”
    Quote in the paperSubstantial claim
  • Findingown data
    § ABSTRACT · p. 1

    The benchmark contains 3,029 Dafny specifications.

    “Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean.”
    Quote in the paperSubstantial claim
  • May combine two claims. 15
  • Classified as probably not a substantial claim. 33

  • May combine two claims.

    Premisecitation
    § 1.1 ORIGINAL SOURCES · p. 14

    The APPS test split instances have more tests per solution and are generally harder than other APPS instances.

    “For APPS, we focused on the 5,000 instances in the test split (Hendrycks et al., 2021), as these have more tests per solution and generally harder tasks.”
    Quote in the paperSubstantial claim1 of 1 sources checked
    • cites Hendrycks et al., 2021 source

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

    Findingnone given
    § 3 BENCHMARK CONSTRUCTION · p. 3

    Verification and vericoding benchmarks are two orders of magnitude smaller than those for theorem proving and vibe coding.

    “Verification and vericoding benchmarks are two orders of magnitude smaller than those for theorem proving and vibe coding.”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    GPT-5 did better than Gemini 2.5 Pro on the 4006 tasks of FV APPS (38.0% vs 12.7%).

    “For instance, we found that GPT-5 did better than Gemini 2.5 Pro on the 4006 tasks of FV APPS (38.0% vs 12.7%).”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4 VERICODING EXPERIMENTS · p. 6

    Conditioned on vericoding success, roughly 9% of the specs were too weak and another 15% had poor translations.

    “Across Dafny, Verus and Lean, conditioned on vericoding success, roughly 9% of the specs were too weak and another 15% had poor translations.”
    Quote in the paperNot a substantial claim

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

    Findingnone given
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    We spent about $25,000 on Open Router.

    “We spent about $25,000 on Open Router.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingreasoning
    § 4.2 PARAMETERS INFLUENCING VERICODING DIFFICULTY · p. 8

    Spec ratio trends fall between these patterns, following solution length trends more closely.

    “Spec ratio trends fall between these patterns, following solution length trends more closely.”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    Translating the Lean verified cogen benchmark (172 tasks) from Verus consumed 1.1M tokens with 99.4% success, while subsequent vericoding attempts required 2.6M tokens, totaling 3.8M tokens for this single benchmark.

    “As an example of computational scale, translating the Lean verified cogen benchmark (172 tasks) from Verus consumed 1.1M tokens with 99.4% success, while subsequent vericoding attempts required 2.6M tokens, totaling 3.8M tokens for this single benchmark.”
    Quote in the paperNot a substantial claim

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

    Findingnone given
    § 1.4 QUALITY ANALYSIS OF SPECIFICATIONS · p. 19

    The high near-duplicates for Bignum Dafny is by design: we split a few big tasks into many smaller ones.

    “The high near-duplicates for Bignum Dafny is by design: we split a few big tasks into many smaller ones.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4 VERICODING EXPERIMENTS · p. 6

    Lean displayed occasional redundant lemma additions during vericoding, and had some weak specs from the original sources.

    “Lean displayed occasional redundant lemma additions during vericoding, and had some weak specs from the original sources.”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § A APPENDIX · p. 14

    The paper ran 55,397 vericoding experiments.

    “contains the outcomes of all 55,397 vericoding experiments, one for each task and each language model.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4 VERICODING EXPERIMENTS · p. 6

    Dafny exhibited no issues except redundant lemmas, with LLMs correctly giving trivial solutions when specs were weak.

    “Dafny exhibited no issues (except for redundant lemmas), with LLMs correctly giving trivial solutions when the specs were weak.”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § A APPENDIX · p. 14

    The benchmark contains 12,504 tasks.

    “contains a summary of the metadata for all 12,504 tasks”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § Dafny (DA0209) · p. 22

    The LLM fills in default values in Verus.

    “The LLM fills in default values in Verus.”
    Quote in the paperNot a substantial claim

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

    Findingown data
    § Dafny (DA0209) · p. 22

    The Dafny spec is an example of an incomplete spec: it does not provide an implementation for some functions such as SplitLinesFunc.

    “The Dafny spec is an example of an incomplete spec: it does not provide an implementation for some functions such as SplitLinesFunc .”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4.1 VERICODING RESULTS · p. 7

    Claude-Opus-4.1 excelled at Dafny, while GPT-5 led on Verus and Lean.

    “Claude-Opus- 4.1 excelled at Dafny, while GPT-5 led on Verus and Lean.”
    Quote in the paperNot a substantial claim

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

    Premisenone given
    § 1 INTRODUCTION · p. 1

    The largest existing formal verification benchmarks contain fewer than 10^3 examples.

    “Unfortunately, formal verification sorely lacks correspondingly large benchmarks: the largest of their kind contain fewer than 10 3 examples.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Study design and conductown data
    § 4 VERICODING EXPERIMENTS · p. 6

    Manual inspection of 5 randomly chosen successful vericoding outputs per language and data source was performed to quantify validity.

    “To quantify the validity of the vericoding process, we perform manual inspection of 5 randomly chosen successful vericoding outputs for each language and data source, noting any LLM behavior that could be considered cheating.”
    Quote in the paperSubstantial claim

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

    Interpretationnone given
    § 4.2 PARAMETERS INFLUENCING VERICODING DIFFICULTY · p. 7

    Helper definitions create interdependent proof obligations that are harder to solve.

    “Helper definitions create interdependent proof obligations that are harder to solve.”
    Quote in the paperNot a substantial claim

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

    Interpretationreasoning
    § 4.2 PARAMETERS INFLUENCING VERICODING DIFFICULTY · p. 8

    With finite iterations per task, shorter implementations allow better use of each iteration.

    “With finite iterations per task, shorter implementations allow better use of each iteration.”
    Quote in the paperNot a substantial claim

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

    Interpretationreasoning
    § 4.2 PARAMETERS INFLUENCING VERICODING DIFFICULTY · p. 7

    More preconditions ease verification by providing assumptions, while more postconditions increase difficulty by requiring additional proofs.

    “More preconditions ease verification by providing assumptions, while more postconditions increase difficulty by requiring additional proofs.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based). May combine two claims.

    Interpretationnone given
    § Lean (LS0012) · p. 22

    The Lean spec provides less information, thus the verus translation is weak as well.

    “The Lean spec provides less information, thus the verus translation is weak as well.”
    Quote in the paperNot a substantial claim

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

    Interpretationreasoning
    § 4.1 VERICODING RESULTS · p. 7

    Lean's lower success probably stems mostly from LLMs being trained primarily on mathematical theorem proving rather than code verification.

    “Lean's lower success probably stems mostly from LLMs being trained primarily on mathematical theorem proving rather than code verification.”
    Quote in the paperNot a substantial claim

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

    Study design and conductnone given
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    The supplementary material includes scripts that can replicate our results.

    “The supplementary material includes scripts that can replicate our results.”
    Quote in the paperNot a substantial claim

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

    Interpretationreasoning
    § 1.5.2 INCOMPLETE CODE · p. 23

    x ∈ result is always false, and result.count x = 1 is also always false, so the spec is satisfied.

    “x ∈ result is always false, and result.count x = 1 is also always false, so the spec is satisfied.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

    Premisecitation
    § 1.1 ORIGINAL SOURCES · p. 14

    Cryptography is a prime target for formal verification.

    “simplified versions of 13 functions often used in cryptography which is a prime target for formal verification (Barbosa et al., 2021).”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites Barbosa et al., 2021 source

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

    Study design and conductnone given
    § 1.6 DAFNYBENCH VERIFICATION · p. 25

    With some models, we weren't able to sample the full 782 problems, so we sampled a random subset as a representative sample.

    “With some models, we weren't able to sample the full 782 problems, so we sampled a random subset as a representative sample.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Study design and conductnone given
    § 1.6 DAFNYBENCH VERIFICATION · p. 25

    To test LLM performance on the original dataset (Loughridge et al., 2025), we use the original prompts and evaluation metrics over n = 10 attempts.

    “To test LLM performance on the original dataset (Loughridge et al., 2025), we use the original prompts and evaluation metrics over n = 10 attempts.”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites Loughridge et al., 2025

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

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

    Interpretationnone given
    § 4.1 VERICODING RESULTS · p. 7

    The lower success on Numpy-Triple is likely due to the mvcgen feature being new.

    “This is likely due to the mvcgen feature being new.”
    Quote in the paperNot a substantial claim

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

    Interpretationnone given
    § 1.6 DAFNYBENCH VERIFICATION · p. 25

    This explains the lower GPT-5 accuracy but higher model union accuracy.

    “This explains the lower GPT-5 accuracy but higher model union accuracy.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Study design and conductown data
    § 3.3 SPEC TRANSLATIONS AND VALIDATION · p. 5

    Benchmark quality was assessed using a scoring framework that penalizes language-specific issues and near-duplicates.

    “We assess benchmark quality using a scoring framework that penalizes language-specific issues and near-duplicates.”
    Quote in the paperSubstantial claim

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

    Interpretationown data
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    This difference is large enough that running on a random sample of 100 tasks will replicate that result.

    “This difference is large enough that running on a random sample of 100 tasks will replicate that result.”
    Quote in the paperNot a substantial claim

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

    Interpretationreasoning
    § 4.2 PARAMETERS INFLUENCING VERICODING DIFFICULTY · p. 8

    Longer specs often contain helper functions that do not require vericoding, unlike additional postconditions which increase difficulty.

    “Additionally, longer specs often contain helper functions that do not require vericoding, unlike additional postconditions which increase difficulty.”
    Quote in the paperSubstantial claim

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

    Study design and conductown data
    § 1.8 REPRODUCIBILITY STATEMENT · p. 25

    The experiments used Dafny 4.11.0, Lean and mathlib v4.23.0-rc2, and Verus and vstd v2025.08.25.

    “The following compiler versions were used in our experiments: - Dafny: 4.11.0 - Lean and mathlib: v4.23.0-rc2 - Verus and vstd: v2025.08.25”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Study design and conductown data
    § 4 VERICODING EXPERIMENTS · p. 5

    The validation tests were designed to detect known proof bypass patterns and LLM cheating strategies.

    “We designed the tests by taking into account known proof bypass patterns (e.g. using sorry for Lean), as well as various LLM cheating strategies that we have identified during our experiments.”
    Quote in the paperSubstantial claim

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

    Study design and conductown data
    § 4 VERICODING EXPERIMENTS · p. 6

    Prompts were not fully optimized.

    “We informally explored prompting variations, but did not optimize the prompts fully.”
    Quote in the paperNot a substantial claim

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

    Study design and conductown data
    § 1.3 PROMPTS AND HYPERPARAMETERS · p. 15

    The evaluation did not run multiple trials with a fresh history.

    “We did not run multiple trials with a fresh history”
    Quote in the paperNot a substantial claim

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

    Study design and conductnone given
    § 5 CONCLUSIONS · p. 8

    The reported vericoding results were achieved without extensive prompt optimization.

    “Our current results, achieved without extensive prompt optimization”
    Quote in the paperNot a substantial claim

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

    Study design and conductnone given
    § 1.1 ORIGINAL SOURCES · p. 14

    Some NumPy specifications have slipped past manual checking and need rechecking.

    “checked by hand (we need to recheck considering some specs have slipped past)”
    Quote in the paperNot a substantial claim

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

    Premisenone given
    § 1 INTRODUCTION · p. 1

    Formal verification remains niche, applied to only a tiny fraction of all software because it requires much more human labor than programming does.

    “Unfortunately, despite a venerable history dating back to Turing (1950), formal verification remains niche, applied to only a tiny fraction of all software because it requires much more human labor than programming does.”
    Quote in the paperNot a substantial claim
39 of 39

  • The authors state this as an assumption.

    AI will soon be able to greatly facilitate formal verification and vericoding, dramatically reducing the cost of creating bug-free software.

    “The premise of this paper is that AI will soon be able to greatly facilitate both, dramatically reducing the cost of creating bug-free software.”

  • The paper relies on this without support.

    Spec repair is an essential part of the formal verification workflow.

    “We include tasks with specs that are incomplete, inconsistent, or non-compilable, because spec repair is an essential part of the formal verification workflow.”

  • The paper relies on this without support.

    LLMs can easily design implementations that pass all unit tests if given the unit tests.

    “Unit tests are not given to the LLM for vericoding, as the LLM can otherwise easily design implementations that pass all unit tests.”

  • The paper relies on this without support.

    The Dafny specifications generated by the LLM translator for APPS are correct.

    “We generated Dafny specifications by means of a specific LLM translator (see Section 3.3).”

  • The paper relies on this without support.

    The translation of the APPS Train split to Lean and addition of formal specs in FVAPPS produces valid vericoding tasks.

    “FVAPPS. It translates the Train split of the APPS Python benchmark to Lean and adds formal specs.”

  • The paper relies on this without support.

    The splitting of DafnyBench files into smaller tasks preserves the original verification challenge.

    “we split the larger files (which contain multiple methods, code and lemmas) into smaller tasks, each with one method and its dependencies.”

  • The paper relies on this without support.

    Removing implementation bodies from Verified Cogen creates valid vericoding tasks.

    “To create tasks, we removed implementation bodies.”

  • The paper relies on this without support.

    Removing spec generation and spec isomorphism requirements from Verina and Clever creates valid vericoding tasks.

    “We removed all spec generation and spec isomorphism requirements from the tasks.”
8 of 8

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

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

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Bursuc et al., 2025

    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

  • VeriCoding's Lean LIS specification attempts a full functional correctness check.

    “The Lean specification in VeriCoding, however, attempts a full functional correctness check.”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Bursuc et al., 2025

    Section 3.1 (p. 4) says VeriCoding tasks provide a specification and require an implementation and proof, supporting the general idea of a formal correctness check. Neither that passage nor the passages found by searching for “LIS” and “longest increasing subsequence” identifies a Lean LIS specification or establishes that it checks full functional correctness. (LLM, conf=0.76)

    Experimental — accuracy not yet measured

  • 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).”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Bursuc et al., 2025

    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

  • VeriCoding's Dafny and Verus LIS specifications ignore the algorithmic logic entirely.

    “They only require the result to be within the array bounds (0 ≤ result ≤ Length), ignoring the algorithmic logic entirely.”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Bursuc et al., 2025

    The manual-inspection discussion (Section 4, p. 6) reports that some Dafny and Verus specifications were weak, but does not identify LIS specifications or state that they require only 0 ≤ result ≤ Length. Searches for LIS, longest increasing subsequence, and the stated result bounds found no passage addressing that specific claim. (LLM, conf=0.72)

    Experimental — accuracy not yet measured

  • VeriCoding's Dafny and Verus LIS specifications only require the result to be within the array bounds (0 ≤ result ≤ Length).

    “They only require the result to be within the array bounds (0 ≤ result ≤ Length), ignoring the algorithmic logic entirely.”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Bursuc et al., 2025

    The manual-inspection discussion (Section 4, p. 6) reports that some Dafny and Verus specifications were too weak, but it does not identify LIS specifications or give their postconditions. Searches for LIS, longest increasing subsequence, and the claimed result bounds found no passage in our copy establishing that these specifications require only 0 ≤ result ≤ Length. (LLM, conf=0.73)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

Each contradiction between two passages listed here was confirmed by an independent check.

  • Conflicting accounts of whether FVAPPS unit tests were applied

    Major

    Section 4.1 says FVAPPS unit tests were not applied in the reported experiments, while the appendix says they were applied in those experiments.

  • Verus overall success rate differs between prose and Table 3

    Minor

    The prose reports 44.2% for Verus, but Table 3 reports 44.3% for the Verus model union at the same precision.

2 of 2

Cites

Flagged first, then by citations

20 of the 49 references couldn’t be matched to a known paper.

Research works printed but not linked: 1

  1. [5]5. Brando Miranda, Zhanke Zhou, Allen Nie, Elyas Obbad, Leni Aniva, Kai Fronsdal, Weston Kirk, Dilara Soylu, Andrea Yu, Ying Li, et al. Veribench: End-to-end formal verification benchmark for ai code generation in lean 4. In 2nd AI for Math Workshop@ ICML 2025 , 2025.

Cited by

Sorted by citations

Authors
Bursuc, S., Ehrenborg, T., Lin, S., Astefanoaei, L., Chiosa, I. E., Kukovec, J., Singh, A., Butterley, O., Bizid, A., Dougherty, Q., Zhao, M., Tan, M., & Tegmark, M.
Affiliations
  • BAIF Development Research Foundation (IN)
  • BAIF
  • Massachusetts Institute of Technology (US)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2025
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2509.22908
arXiv
2509.22908
OpenAlex
W7083815470
Semantic Scholar
d048ae5afdfedd33f099d6e5d9ab918f86e37564
Cited by
1
References
49
Citations by year
2026: 1
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
  • Physical Sciences › Computer Science › Computer Science Applications › Teaching and Learning Programming
Keywords
program synthesis, formal verification, LLM-based code generation, benchmark, Dafny, Verus, Rust, lean manufacturing, formal specification, vibe coding, natural language descriptions

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Claims read by deepseek-v4.1-flash under definition version 3 (extract-v3) on 2026-10-24.

Classified by jev-1.13-20260917 (gold-guideline-v0.2) on 2026-10-24.

Cited sources are checked by gpt-6-sol.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review