VERINA: Benchmarking Verifiable Code Generation

Ye, Zhe; Yan, Zhengxu; He, Jingxuan; Kasriel, Timothe; Yang, Kaiyu; Song, Dawn

doi:10.48550/arxiv.2505.23135

PreprintCited by 7Software Engineering ResearchLogic, programming, and type systemsSoftware Testing and Debugging Techniques

VERINA: Benchmarking Verifiable Code Generation

Open access

Ye, Zhe, Yan, Zhengxu, He, Jingxuan, Kasriel, Timothe, Yang, Kaiyu, Song, Dawn·2025·arXiv

DOI 10.48550/arxiv.2505.23135arXiv 2505.23135

Open this paper in CoChat — free account Open PDF

Abstract

Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often focus on only individual components rather than providing a holistic evaluation framework of all tasks. In this paper, we introduce VERINA (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o3, achieves a 72.6\% code correctness rate, 52.3\% for specification soundness and completeness, and a mere 4.9\% proof success rate (based on one trial per task). We hope VERINA will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.

AI snapshot

Written from the paper’s full text.

TL;DR

VERINA is a 189-task Lean benchmark for modular evaluation of code, specification, and proof generation, including their combinations. It finds proof generation remains extremely difficult for state-of-the-art LLMs, with the best model, OpenAI o4-mini, achieving only 3.6% successful proofs.

Key findings

VERINA contains 189 manually curated Lean coding tasks with natural-language descriptions, reference implementations, formal specifications, and test suites; 46 of 189 examples also have manually written ground-truth proofs.
The best model, OpenAI o4-mini, generates 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task.
Proof generation is the hardest foundational task: pass@1 rates are below 3.6% for all evaluated models. Iterative proof refinement improves o4-mini from 7.41% to 22.22% on VERINA-BASIC after 64 iterations, but gains are much smaller on VERINA-ADV (1.23% to 6.17%).
Providing ground-truth specifications consistently improves CodeGen, while providing ground-truth code shows minimal or negative improvement for SpecGen; using LLM-generated code or specifications as context generally degrades performance.

Methods

Benchmark construction: VERINA-BASIC combines 49 manually translated MBPP-DFY-50 Dafny problems and 59 CloverBench Dafny instances translated into Lean with OpenAI o3-mini few-shot prompting followed by manual inspection and correction. VERINA-ADV consists of 81 selected and manually reviewed student Lean submissions adapted from theorem-proving and program-verification coursework.
Evaluation covers three foundational tasks—CodeGen, SpecGen, and ProofGen—and their combinations. CodeGen is evaluated by positive tests and pass@k; ProofGen is checked by Lean, with proofs containing placeholders such as `sorry` marked incorrect; SpecGen soundness and completeness are evaluated through a testing-based Lean framework using `decide` and property-based testing with `plausible`, with error bars for unknown outcomes.
Experimental setup: nine state-of-the-art LLMs are evaluated with 2-shot prompting, five samples per instance, pass@1 primarily reported, temperature 1.0, and a 10,000-token maximum output budget. Iterative proof refinement is evaluated for four best-performing models up to 64 rounds.

Limitations

The paper states that VERINA’s size (189 examples) is modest; scaling to a larger dataset suitable for finetuning likely requires automated annotation with LLM assistance. It also states that VERINA emphasizes simple, standalone tasks that are not fully representative of complex real-world verification projects, and that the SpecGen metric could be improved by more capable provers, including LLM- or SMT-based provers, to prove soundness/completeness relationships. The paper also notes a risk of data contamination because underlying task topics are drawn from widely used sources.
The text makes evident that the SpecGen evaluation is testing-based: it can prove a relationship does not hold via counterexamples but cannot formally establish that it holds, and it returns unknown for some complicated quantified specifications. The paper also notes that it does not yet check for definitional equivalence in end-to-end verifiable code generation, leaving that as future work.

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

Integrity signals

Registry

DataCite · 10.48550/arxiv.2505.23135

Cites

55 of 55 references verified0 citation errors · 0 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

0 of 8 cited sources checked · 0 supported · 0 flagged

Findingnone given
VERINA consists of 189 standalone programs, annotated with natural language descriptions, code, specifications, proofs, and test cases.
“VERINA consists of 189 standalone programs, annotated with natural language descriptions, code, specifications, proofs, and test cases.”
Quote in the paperSubstantial claim
Findingnone given
VERINA provides 189 high-quality samples with varying difficulty levels.
“In contrast, VERINA provides 189 high-quality samples with varying difficulty levels.”
Quote in the paperSubstantial claim
Findingown data
o4-mini improves from 7.41% to 22.22% on VERINA-BASIC after 64 iterations of iterative proof refinement.
“with o4-mini improving from 7.41% to 22.22% on VERINA-BASIC after 64 iterations.”
Quote in the paperSubstantial claim
Findingown data
Generating sound and complete post-conditions is generally more difficult than pre-conditions.
“We report detailed results on pre-condition and post-condition soundness and completeness in Appendix B, where we observe that generating sound and complete post-conditions is generally more difficult than pre-conditions.”
Quote in the paperNot a substantial claim
Findingown data
Iterative proof refinement yields meaningful improvements on simpler problems.
“Iterative proof refinement shows meaningful improvements.”
- Also stated in: § 5 Experimental Evaluation · plain
  “As shown in Figure 7, iterative proof refinement yields meaningful improvements on simpler problems, with o4-mini improving from 7.41% to 22.22% on VERINA-BASIC after 64 iterations.”
Quote in the paperSubstantial claim

Findingown data
Among the evaluated models, o4-mini, GPT 4.1, Claude Sonnet 3.7, and Gemini 2.5 Flash demonstrate relatively stronger performance across tasks.
“Among the evaluated models, o4-mini, GPT 4.1, Claude Sonnet 3.7, and Gemini 2.5 Flash demonstrate relatively stronger performance across tasks.”
Quote in the paperNot a substantial claim
Findingown data
The extensive evaluation results present substantial challenges that expose limitations of state-of-the-art language models on verifiable code generation tasks.
“our extensive evaluation result presents substantial challenges that expose limitations of state-of-the-art language models on verifiable code generation tasks.”
Quote in the paperSubstantial claim
Findingreasoning
When using LLM-generated code or specifications as context instead of ground truth, performance generally degrades.
“Furthermore, when using LLM-generated code or specifications as context instead of ground truth, performance generally degrades.”
Quote in the paperSubstantial claim
Findingnone given
Comparing refinements and direct generation without error messages demonstrates the clear value of Lean verifier feedback.
“Furthermore, comparing refinements and direct generation without error messages demonstrates the clear value of Lean verifier feedback.”
Quote in the paperNot a substantial claim
Findingown data
Gains from iterative proof refinement are substantially less on VERINA-ADV (1.23% to 6.17%).
“However, these gains are substantially less on VERINA-ADV (1.23% to 6.17%), indicating that naive refinement strategies are insufficient for complex proving tasks.”
Quote in the paperSubstantial claim
Findingown data
Manual inspection of evaluation results reveals no evidence of LLMs directly using ground truth code in the specification.
“While it is possible for LLMs to directly use the ground truth code in the specification, manual inspection of our evaluation results reveals no evidence of such behaviors.”
Quote in the paperSubstantial claim
Findingown data
Providing ground truth code as context shows minimal or negative improvement for SpecGen.
“On the contrary, providing ground truth code as context shows minimal or negative improvement for SpecGen.”
Quote in the paperSubstantial claim
Findingreasoning
VERINA-ADV enhances the diversity of VERINA by incorporating more advanced coding problems and solutions.
“VERINA-ADV enhances the diversity of VERINA by incorporating more advanced coding problems and solutions.”
Quote in the paperNot a substantial claim
Findingnone given
VERINA consists of two subsets sourced from different origins: VERINA-BASIC and VERINA-ADV.
“VERINA consists of two subsets sourced from different origins: VERINA-BASIC and VERINA-ADV.”
Quote in the paperNot a substantial claim
Findingown data
Providing ground truth specifications as context consistently improves CodeGen performance across models.
“Providing ground truth specification benefits CodeGen.”
- Also stated in: § 5 Experimental Evaluation · boosted
  “Providing ground truth specifications as context consistently improves CodeGen performance across models.”
Quote in the paperSubstantial claim
Findingown data
LLMs can generate specifications that are too restrictive, leading to unsound pre-conditions.
“Figure 15 demonstrates how LLMs can generate specifications that are too restrictive, leading to unsound pre-conditions.”
Quote in the paperSubstantial claim
Findingreasoning
This unsound specification would accept invalid outputs like [2, 1, 0] representing 012, which should be rejected in favor of [2,1].
“This unsound specification would accept invalid outputs like [2, 1, 0] representing 012 (which is one of the negative test case), which should be rejected in favor of [2,1].”
Quote in the paperSubstantial claim
Findingown data
After 23 failed refinement attempts, o4-mini makes useful improvements based on Lean compiler error messages, significantly restructuring its approach.
“After 23 failed refinement attempts, the model makes useful improvements based on Lean compiler error messages, significantly restructuring its approach.”
Quote in the paperNot a substantial claim
Findingown data
LLMs can generate overly permissive preconditions that fail to capture essential constraints.
“Figure 16 demonstrates how LLMs can generate overly permissive preconditions that fail to capture essential constraints.”
Quote in the paperSubstantial claim
Findingown data
Figure 19 demonstrates the limitations of the testing-based evaluation framework when encountering specifications with quantifiers over complicated structures or infinite domains.
“Figure 19 demonstrates the limitations of our testing-based evaluation framework when encountering specifications with quantifiers over complicated structures or infinite domains.”
Quote in the paperSubstantial claim
Findingown data
o4-mini generates an unsound postcondition that fails to rule out leading zeros in the result (verina_advanced_5).
“Example (verina_advanced_5): o4-mini generates unsound postcondition that fails to rule out leading zeros in the result.”
Quote in the paperNot a substantial claim
Findingown data
The ground truth post-condition for the smallest single-digit prime factor task correctly handles all cases, including the edge case where n = 0, specifying that the result should be 0 when the input is 0 or when no single-digit prime divides n.
“The ground truth post-condition correctly handles all cases including the edge case where n = 0, specifying that the result should be 0 when the input is 0 or when no single-digit prime divides n.”
Quote in the paperSubstantial claim
Findingown data
LLMs can generate post-conditions that miss critical constraints, leading to unsound specifications.
“Figure 17 illustrates how LLMs can generate post-conditions that miss critical constraints, leading to unsound specifications.”
Quote in the paperSubstantial claim
Findingreasoning
Since the LLM-generated pre-condition accepts this negative test case, the evaluation metric determines that the LLM-generated pre-condition is incomplete.
“Since the LLM-generated pre-condition accepts this negative test case, our evaluation metric determines that the LLM-generated pre-condition is incomplete.”
Quote in the paperSubstantial claim
Findingreasoning
The evaluation framework returns unknown for specifications with unbounded quantification, as neither decidable testing nor plausible exploration can adequately handle it.
“Our evaluation framework returns unknown for such cases, as neither decidable testing nor plausible exploration can adequately handle the unbounded quantification.”
Quote in the paperSubstantial claim
Findingown data
The substantial performance gap between preconditions and postconditions confirms that generating complex input-output relationships remains significantly more challenging than input validation constraints.
“the substantial performance gap between preconditions and postconditions confirms that generating complex input-output relationships remains significantly more challenging than input validation constraints.”
Quote in the paperSubstantial claim
Findingreasoning
The LLM-generated version uses strict inequality k < (distinct nums).length, which incorrectly excludes valid cases where k equals the total number of distinct elements.
“However, the LLM-generated version uses strict inequality k < (distinct nums).length,which incorrectly excludes valid cases where k equals the total number of distinct elements.”
Quote in the paperSubstantial claim
Findingown data
o4-mini generates a nextGreaterOne helper function with a bug in the state management logic.
“o4-mini generates a nextGreaterOne helper function with a bug in the state management logic.”
Quote in the paperNot a substantial claim
Findingreasoning
This makes the precondition unsound as it rejects legitimate inputs that should be accepted by the specification.
“This makes the precondition unsound as it rejects legitimate inputs that should be accepted by the specification.”
Quote in the paperSubstantial claim
Findingown data
o4-mini hallucinates the Int.xor method that does not exist in Lean 4's standard library.
“it hallucinates the Int.xor method that does not exist in Lean 4's standard library.”
Quote in the paperNot a substantial claim
Findingown data
o4-mini generates code that appears syntactically correct but contains non-existent methods.
“Figure 13 demonstrates a common LLM failure mode where o4-mini generates code that appears syntactically correct but contains non-existent methods.”
Quote in the paperNot a substantial claim
Findingown data
The LLM-generated post-condition omits the leading zero constraint entirely, only checking that the result is non-empty and digits are valid.
“However, the LLM-generated post-condition omits the leading zero constraint entirely, only checking that the result is non-empty and digits are valid.”
Quote in the paperSubstantial claim
Findingown data
The drop in performance when requiring both soundness and completeness simultaneously-compared to achieving either individually-demonstrates that partial correctness is insufficient.
“the drop in performance when requiring both soundness and completeness simultaneously-compared to achieving either individually-demonstrates that partial correctness is insufficient and justifies our comprehensive evaluation framework for specification quality.”
Quote in the paperSubstantial claim
Findingnone given
o4-mini generates a post-condition with quantifiers over lists that cannot be evaluated by plausible testing (verina_advanced_25).
“Example (verina_advanced_25): o4-mini generates post-condition with quantifiers over lists that cannot be evaluated by plausible testing.”
Quote in the paperNot a substantial claim
Findingown data
This makes the precondition incomplete as it accepts invalid inputs that violate the problem's fundamental assumptions.
“This makes the precondition incomplete as it accepts invalid inputs that violate the problem's fundamental assumptions, potentially leading to incorrect behavior in the implementation and proof generation phases.”
Quote in the paperSubstantial claim
Findingown data
o4-mini generates code with a logical error in state management, causing unit test failure (verina_advanced_57).
“Example (verina_advanced_57): o4-mini generates code with logical error in state management, causing unit test failure.”
Quote in the paperNot a substantial claim
Findingown data
o4-mini generates an unsound pre-condition using strict inequality instead of allowing k to equal the number of distinct elements (verina_advanced_76).
“Example (verina_advanced_76): o4-mini generates unsound pre-condition using strict inequality instead of allowing k to equal the number of distinct elements.”
Quote in the paperNot a substantial claim
Findingown data
Syntax incorrectness and use of non-existent library functions represent the major problems, especially for less capable models.
“They reveal that syntax incorrectness and use of non-existent library functions (as demonstrated in Appendix C) represent the major problems, especially for less capable models.”
Quote in the paperNot a substantial claim
Findingown data
o4-mini generates an incomplete pre-condition using True instead of enforcing uniqueness and subset constraints (verina_advanced_57).
“Example (verina_advanced_57): o4-mini generates incomplete pre-condition using True instead of enforcing uniqueness and subset constraints.”
Quote in the paperNot a substantial claim
Findingown data
The LLM-generated precondition simply uses True, completely ignoring all stated constraints.
“However, the LLM-generated precondition simply uses True, completely ignoring all stated constraints.”
Quote in the paperNot a substantial claim
Findingown data
Initially, o4-mini generates an overly simple proof using direct induction and simp tactics, which fails to handle the complex logical structure.
“Initially, o4-mini generates an overly simple proof using direct induction and simp tactics, which fails to handle the complex logical structure.”
Quote in the paperNot a substantial claim
Findingown data
The LLM-generated post-condition for the smallest single-digit prime factor task fails to consider n = 0 entirely.
“However, the LLM-generated post-condition fails to consider n = 0 entirely.”
Quote in the paperSubstantial claim
Findingown data
Achieving simultaneous soundness and completeness poses great challenge, particularly for post-conditions.
“Achieving simultaneous soundness and completeness poses great challenge, particularly for post-conditions.”
Quote in the paperSubstantial claim
Findingown data
LLMs can generate post-conditions that are both unsound and incomplete by failing to handle edge cases properly, as demonstrated in Figure 18.
“Figure 18 demonstrates how LLMs can generate post-conditions that are both unsound and incomplete by failing to handle edge cases properly.”
Quote in the paperNot a substantial claim
Findingown data
o4-mini generates an unsound and incomplete postcondition that fails to handle the edge case n = 0 (verina_advanced_72).
“Example (verina_advanced_72): o4-mini generates unsound and incomplete postcondition that fails to handle the edge case n = 0.”
Quote in the paperNot a substantial claim
Premisereasoning
All other prior works lack compositionality.
“On the contrary, all other prior works lack compositionality.”
Quote in the paperNot a substantial claim
Interpretationreasoning
A key strength of VERINA is its modular design, which enables flexible evaluation of not only individual tasks but also their combinations.
“A key strength of VERINA is its modular design, which enables flexible evaluation of not only individual tasks but also their combinations.”
Quote in the paperSubstantial claim
Interpretationown data
Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation.
“Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains.”
Quote in the paperSubstantial claim
Interpretationnone given
VERINA is a high-quality benchmark enabling comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
“In this paper, we introduce VERINA (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.”
Quote in the paperSubstantial claim
Interpretationown data
With a median of 5 positive tests and 12 negative tests per instance, the constructed test suites provide strong evidence for the high quality and correctness of VERINA.
“With a median of 5 positive tests and 12 negative tests per instance, the constructed test suites provide strong evidence for the high quality and correctness of VERINA.”
Quote in the paperNot a substantial claim
Study design and conductreasoning
When designing VERINA's tasks, we enforce independence-for example, the model cannot access the code when generating the specification.
“When designing VERINA's tasks, we enforce independence-for example, the model cannot access the code when generating the specification.”
Quote in the paperSubstantial claim
- Rests on an assumption: The model cannot access the code when generating the specification ensures independence.
Interpretationown data
Verbose code implementations may introduce noise to or over-constrain specification generation rather than providing helpful guidance.
“The asymmetry in using ground truth information for CodeGen versus SpecGen suggests that formal specifications effectively constrain and guide code synthesis, while verbose code implementations may introduce noise to or over-constrain specification generation rather than providing helpful guidance.”
Quote in the paperSubstantial claim
Interpretationnone given
VERINA enables comprehensive evaluation of verifiable code generation, covering foundational tasks and their combinations.
“VERINA enables comprehensive evaluation of verifiable code generation, covering foundational tasks-code, specification, and proof generation-and their combinations to form an end-to-end pipeline from natural language descriptions to verifiable code.”
Quote in the paperSubstantial claim
Interpretationreasoning
Combined tasks, where LLMs must generate both code and specifications jointly, might be significantly more challenging than individual tasks in isolation.
“This suggests that combined tasks, where LLMs must generate both code and specifications jointly, might be significantly more challenging than individual tasks in isolation.”
Quote in the paperNot a substantial claim
Study design and conductreasoning
We crafted all ground truth specifications such that they cannot be directly used to solve the coding problem.
“We crafted all ground truth specifications such that they cannot be directly used to solve the coding problem.”
Quote in the paperSubstantial claim
Study design and conductnone given
We carefully selected the most suitable and high-quality submissions, resulting in 81 benchmark instances.
“We carefully selected the most suitable and high-quality submissions, resulting in 81 benchmark instances.”
Quote in the paperSubstantial claim
Interpretationreasoning
This prevents LLMs from generating an implementation trivially equivalent to the specification.
“This prevents LLMs from generating an implementation trivially equivalent to the specification.”
Quote in the paperSubstantial claim
Study design and conductreasoning
Since our evaluator is based on testing, it can prove that R does not hold through counterexamples.
“Since our evaluator is based on testing, it can prove that R does not hold through counterexamples, as highlighted in green in Figure 3.”
Quote in the paperSubstantial claim
Interpretationreasoning
For any combined task involving ProofGen, LLMs' performance will be heavily bottlenecked by the ProofGen subtask.
“This also means that for any combined task involving ProofGen, LLMs' performance will be heavily bottlenecked by the ProofGen subtask.”
Quote in the paperNot a substantial claim
Interpretationreasoning
All CodeGen improvements from providing ground truth specifications rely on semantic understanding of the reference specification.
“Since the ground truth specifications cannot be used directly as code (as explained in 3.2), all CodeGen improvements rely on semantic understanding of the reference specification.”
Quote in the paperSubstantial claim
Interpretationown data
Problem complexity significantly impacts all aspects of verifiable code generation.
“This demonstrates that problem complexity significantly impacts all aspects of verifiable code generation, and VERINA-ADV provides a valuable challenge for advancing future research in this domain.”
Quote in the paperSubstantial claim
Interpretationreasoning
The generated artifacts can be of insufficient quality to serve as reliable reference.
“The generated artifacts can be of insufficient quality to serve as reliable reference.”
Quote in the paperSubstantial claim
Premisecitation
Existing tools do not adequately model the necessary Lean features.
“Another approach is to convert these relationships into ATP; however, existing tools do not adequately model the necessary Lean features [43].”
Quote in the paperSubstantial claim0 of 1 sources checked
- cites [43]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Interpretationown data
Naive refinement strategies are insufficient for complex proving tasks.
“However, these gains are substantially less on VERINA-ADV (1.23% to 6.17%), indicating that naive refinement strategies are insufficient for complex proving tasks.”
Quote in the paperSubstantial claim
Interpretationown data
Formal specifications effectively constrain and guide code synthesis.
“The asymmetry in using ground truth information for CodeGen versus SpecGen suggests that formal specifications effectively constrain and guide code synthesis, while verbose code implementations may introduce noise to or over-constrain specification generation rather than providing helpful guidance.”
Quote in the paperSubstantial claim
Study design and conductreasoning
VERINA addresses the challenge of capturing human intent by leveraging high-quality ground truth specifications and comprehensive test suites.
“VERINA addresses this by leveraging high-quality ground truth specifications (see Section 3.2) and comprehensive test suites.”
Quote in the paperSubstantial claim
- Rests on an assumption: The ground truth specifications accurately capture human intent.
Interpretationown data
Current LLMs fall short in understanding Lean 4's language features.
“This shows that current LLMs fall short in understanding Lean 4's language features.”
Quote in the paperNot a substantial claim
Study design and conductreasoning
Deciding the soundness of P is equivalent to verifying whether P (x) holds for all positive tests x in the test suite.
“Deciding the soundness of P is equivalent to verifying whether P (x) holds for all positive tests x in our test suite.”
Quote in the paperSubstantial claim
Study design and conductreasoning
The soundness of Q can be evaluated using negative test cases.
“The soundness of Q can be evaluated using our negative test cases.”
Quote in the paperSubstantial claim
Interpretationown data
The missing edge case handling in the LLM-generated post-condition demonstrates how LLMs may overlook corner cases that are crucial for specification completeness (and soundness).
“The missing edge case handling demonstrates how LLMs may overlook corner cases that are crucial for specification completeness (and soundness).”
Quote in the paperSubstantial claim
Interpretationown data
The missing constraint demonstrates how LLMs may capture the primary functional requirements while overlooking more subtle constraints that are crucial for correctness.
“The missing constraint demonstrates how LLMs may capture the primary functional requirements while overlooking more subtle constraints that are crucial for correctness.”
Quote in the paperSubstantial claim
Study design and conductown data
In the test suites, there is a positive test case with nums = [5] and k = 1.
“In our test suites, we have a positive test case with nums = [5] and k = 1.”
Quote in the paperSubstantial claim
Study design and conductown data
The relatively low unknown percentages across most evaluations demonstrate that the specification evaluation metric is reliable.
“The relatively low unknown percentages across most evaluations demonstrate that our specification evaluation metric is reliable.”
Quote in the paperNot a substantial claim
Interpretationreasoning
When n = 0, the condition n % p ̸ = 0 is false for any prime p (since 0 % p = 0), making the first disjunct of the LLM-generated post-condition impossible to satisfy.
“When n = 0, the condition n % p ̸ = 0 is false for any prime p (since 0 % p = 0), making the first disjunct impossible to satisfy.”
Quote in the paperSubstantial claim
Study design and conductreasoning
The completeness of Q can be evaluated using positive test cases.
“The completeness of Q can be evaluated using our positive test cases.”
Quote in the paperSubstantial claim
Study design and conductreasoning
Deciding the completeness of P is equivalent to verifying whether P (x) does not hold for all negative tests x in the test suite.
“Similarly, deciding the completeness of P is equivalent to verifying whether P (x) does not hold for all negative tests x in our test suite.”
Quote in the paperSubstantial claim
Interpretationreasoning
This example highlights a fundamental challenge in automatically evaluating LLM-generated formal specifications.
“This example highlights a fundamental challenge in automatically evaluating LLM-generated formal specifications”
Quote in the paperNot a substantial claim
Interpretationnone given
The evaluation framework successfully handles most practical cases.
“while our framework successfully handles most practical cases”
Quote in the paperSubstantial claim
Study design and conductown data
In the test suites, there is a negative test case with nums1 = [1,1] and nums2 = [1,2].
“In our test suites, we have a negative test case with nums1 = [1,1] and nums2 = [1,2].”
Quote in the paperSubstantial claim

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

May combine two claims.
Findingown data
The best model, OpenAI o4-mini, generates only 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task.
“The best model, OpenAI o4-mini, generates only 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task.”
Quote in the paperSubstantial claim
May combine two claims.
Findingown data
Code ranges up to 38 lines and specifications up to 62 lines.
“Code ranges up to 38 lines and specifications up to 62 lines, demonstrating that VERINA captures complex tasks.”
Quote in the paperSubstantial claim
May combine two claims.
Findingnone given
VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites.
“VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites.”
Quote in the paperSubstantial claim
May combine two claims.
Findingreasoning
VERINA provides high-quality, human-verified samples and captures all three foundational tasks in verifiable code generation.
“In contrast, VERINA provides high-quality, human-verified samples and captures all three foundational tasks in verifiable code generation.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
Natural language descriptions have a median length of 110 words.
“Natural language descriptions have a median length of 110 words, ensuring they are both informative and detailed.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingreasoning
Ground truth proofs are optional in VERINA, as they are not required for evaluation.
“Ground truth proofs are optional in VERINA, as they are not required for evaluation.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim. May combine two claims.
Findingnone given
The code, specification, and proof are all written in Lean.
“The code, specification, and proof are all written in Lean.”
Quote in the paperSubstantial claim
May combine two claims.
Findingown data
Code generation achieves the highest success rates across models, followed by specification generation, while proof generation remains the most challenging with pass@1 rates below 3.6% for all models.
“Code generation achieves the highest success rates across models, followed by specification generation, while proof generation remains the most challenging with pass@1 rates below 3.6% for all models.”
Quote in the paperSubstantial claim
May combine two claims.
Findingown data
VERINA-ADV is much more challenging than VERINA-BASIC, with substantial difficulty gaps on all three tasks.
“VERINA-ADV is much more challenging than VERINA-BASIC.”
- Also stated in: § 5 Experimental Evaluation · plain
  “The comparison between VERINA-BASIC and VERINA-ADV in Figure 6 reveals substantial difficulty gaps on all three tasks.”
Quote in the paperSubstantial claim
May combine two claims.
Findingown data
For VERINA-BASIC, the maximum (median) LoC for code and specification are 26 (6) and 17 (2), respectively.
“For VERINA-BASIC, the maximum (median) LoC for code and specification are 26 (6) and 17 (2), respectively.”
Quote in the paperNot a substantial claim
May combine two claims.
Findingnone given
VERINA is a comprehensive benchmark comprising 189 carefully curated examples with detailed task descriptions, high-quality codes and specifications in Lean, and extensive test suites with full line coverage.
“We have introduced VERINA, a comprehensive benchmark comprising 189 carefully curated examples with detailed task descriptions, high-quality codes and specifications in Lean, and extensive test suites with full line coverage.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Findingreasoning
While Lean programs in VERINA are newly written, the underlying task topics are drawn from widely used sources, posing a risk of data contamination.
“Finally, while Lean programs in VERINA are newly written, the underlying task topics are drawn from widely used sources, posing a risk of data contamination.”
Quote in the paperNot a substantial claim
May combine two claims.
Findingown data
All ground truth specifications successfully pass their respective positive tests, confirming the quality of the specifications in VERINA.
“All ground truth specifications successfully pass their respective positive tests, confirming the quality of the specifications in VERINA.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).
Findingnone given
VERINA-ADV is much more challenging than VERINA-BASIC.
“VERINA-ADV is much more challenging than VERINA-BASIC.”
Quote in the paperNot a substantial claim
May combine two claims.
Findingown data
For VERINA-ADV, the maximum (median) LoC for code and specification are 38 (16) and 62 (7), respectively.
“For VERINA-ADV, they are 38 (16) and 62 (7).”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
o4-mini generates a correct proof on the 24th attempt (verina_advanced_64).
“Example (verina_advanced_64): o4-mini generates correct proof on the 24th attempt.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingreasoning
This results in incorrect outputs for the test case where nums1 = [1, 2, 3] and nums2 = [3, 2, 1, 4] should return [4, 4, 4].
“This results in incorrect outputs for the test case where nums1 = [1, 2, 3] and nums2 = [3, 2, 1, 4] should return [4, 4, 4].”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
o4-mini generates an incorrect proof on the first attempt (verina_advanced_64).
“Example (verina_advanced_64): o4-mini generates incorrect proof on the first attempt.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Findingreasoning
Since the LLM-generated pre-condition rejects this test case, the evaluation metric determines that it is unsound.
“Since the LLM-generated pre-condition rejects this test case, our evaluation metric determines that it is unsound.”
Quote in the paperNot a substantial claim
May combine two claims.
Findingown data
After finding the target element, the function incorrectly calls aux tl false instead of aux tl true in Line 22, causing it to lose track of having found the target and fail to identify subsequent greater elements.
“After finding the target element, the function incorrectly calls aux tl false instead of aux tl true in Line 22, causing it to lose track of having found the target and fail to identify subsequent greater elements.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Findingown data
DeepSeek Prover 2 7B and Qwen 3 235B-A22B-FP8 suffer from instruction following ability, failing to output the desired format specified in the prompts.
“DeepSeek Prover 2 7B and Qwen 3 235B-A22B-FP8 suffer from instruction following ability, failing to output the desired format specified in our prompts (cf.Appendix A.3).”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
o4-mini generates an incorrect proof after 23 refinement attempts (verina_advanced_64).
“Example (verina_advanced_64): o4-mini generates incorrect proof after 23 refinement attempts.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
Figures 20, 21, 22, and 23 demonstrate o4-mini's iterative proof refinement process over 24 attempts.
“Figure 20, 21, 22, and 23 demonstrate o4mini's iterative proof refinement process over 24 attempts.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingown data
The error message from the 23rd refinement attempt reveals that the proof got stuck on conditional expressions involving decide predicates.
“The error message from the 23rd attempt reveals that the proof got stuck on conditional expressions involving decide predicates.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Findingreasoning
The ground truth precondition correctly enforces three critical requirements: List.Nodup nums1 ensures uniqueness in the first array, List.Nodup nums2 ensures uniqueness in the second array, and nums1.all(fun x => x ∈ nums2) verifies that nums1 is indeed a subset of nums2.
“The ground truth precondition correctly enforces three critical requirements: List.Nodup nums1 ensures uniqueness in the first array, List.Nodup nums2 ensures uniqueness in the second array, and nums1.all(fun x => x ∈ nums2) verifies that nums1 is indeed a subset of nums2.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Findingnone given
VERINA contains more difficult instances than the one presented in Figure 1.
“Note that we select this instance for presentation purposes and VERINA contains more difficult ones.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.
Findingnone given
More capable models often generate specifications with more complicated logical structures, leading to higher unknown percentages in post-condition evaluation.
“More capable models often generate specifications with more complicated logical structures, leading to higher unknown percentages in post-condition evaluation.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim. May combine two claims.
Findingnone given
The ground truth postcondition correctly enforces three essential properties: arithmetic correctness, digit validity (each digit < 10), and prohibition of leading zeros except for the special case where the result is zero.
“The ground truth postcondition correctly enforces three essential properties: arithmetic correctness, digit validity (each digit < 10), and prohibition of leading zeros except for the special case where the result is zero.”
Quote in the paperSubstantial claim
May combine two claims.
Findingown data
In the successful 24th attempt, o4-mini improves its strategy by introducing an auxiliary lemma helper_eq_filter and using explicit case analysis with by_cases.
“In the successful 24th attempt, o4-mini improves its strategy by introducing an auxiliary lemma helper_eq_filter and using explicit case analysis with by_cases.”
Quote in the paperNot a substantial claim
May combine two claims.
Findingreasoning
The LLM-generated post-condition for the smallest single-digit prime factor task rejects the positive test case (n=0, result=0) and accepts the negative test case (n=0, result=2), so the evaluation metric determines it is both unsound and incomplete.
“The LLM-generated post-condition rejects the positive test case and accepts the negative test case, therefore our evaluation metric determines that this generated post-condition is both unsound and incomplete.”
Quote in the paperSubstantial claim
May combine two claims.
Findingreasoning
Pre-conditions are generally simpler than post-conditions, resulting in lower unknown rates during evaluation.
“Pre-conditions are generally simpler than post-conditions, resulting in lower unknown rates during evaluation.”
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
Model-generated proofs can be checked by Lean directly.
“Modelgenerated proofs can be checked by Lean directly.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Study design and conductreasoning
We invest significant manual effort in writing proofs for 46 out of 189 examples as they help quality assurance.
“Nevertheless, we invest significant manual effort in writing proofs for 46 out of 189 examples as they help quality assurance (Section 3.2).”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim. May combine two claims.
Study design and conductnone given
Generated proofs are directly evaluated using the Lean compiler and any proofs containing placeholders are filtered out.
“We directly evaluate generated proofs using the Lean compiler and filter out any proofs containing placeholders, as described in Section 4.1.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S4 (based).
Study design and conductnone given
We introduce a novel framework for a reliable automatic evaluation of model-generated specifications.
“We also introduce a novel framework for a reliable automatic evaluation of model-generated specifications.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductnone given
VERINA involves no model training or fine-tuning processes.
“VERINA involves no model training or fine-tuning processes.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductreasoning
We leveraged the standard coverage.py tool to verify complete line coverage.
“We leveraged the standard coverage.pytool to verify complete line coverage, since Lean lacks a robust coverage tool.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim.
Study design and conductcitation
For each problem instance, 5 responses are sampled from each model and pass@1 metrics are calculated using these 5 samples to ensure robust evaluation statistics.
“For each problem instance, we sample 5 responses from each model and calculate pass@1 metrics [3] using these 5 samples to ensure robust evaluation statistics.”
Quote in the paperSubstantial claim0 of 1 sources checked
- cites [3]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
May combine two claims.
Interpretationown data
While it cannot formally establish R holds, it remains highly robust in this regard, due to our comprehensive test suite with both positive and negative tests, which achieve full coverage on ground truth code implementations.
“While it cannot formally establish R holds, it remains highly robust in this regard, due to our comprehensive test suite with both positive and negative tests, which achieve full coverage on ground truth code implementations.”
Quote in the paperSubstantial claim
- Rests on an assumption: The test suites are comprehensive enough to serve as a reliable proxy for formal verification of specification soundness and completeness.
Probably not a substantial claim: may not pass S3 (load-bearing).
Premisecitation
MBPP-DFY-50 is licensed under GPL-3.0.
“MBPP-DFY-50 [18] is licensed under GPL-3.0”
Quote in the paperNot a substantial claim0 of 1 sources checked
- cites [18]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductnone given
The 2-shot examples are excluded from the final benchmark evaluation.
“The 2-shot examples are excluded from the final benchmark evaluation.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim.
Interpretationreasoning
In end-to-end verifiable code generation, it is crucial that the model generates code and specification independently, rather than sequentially.
“In end-to-end verifiable code generation, it is crucial that the model generates code and specification independently, rather than sequentially.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).
Interpretationnone given
Overall, the coding difficulty in VERINA-BASIC, abstracting away language differences, is comparable to MBPP.
“Overall, the coding difficulty in VERINA-BASIC, abstracting away language differences, is comparable to MBPP.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim. May combine two claims.
Study design and conductnone given
We use Lean to automatically check the validity of generated proofs, and proofs containing placeholders (e.g., the sorry tactic) are marked as incorrect.
“We use Lean to automatically check the validity of generated proofs, and proofs containing placeholders (e.g., the sorry tactic) are marked as incorrect.”
Quote in the paperSubstantial claim
May combine two claims.
Study design and conductnone given
We manually translated 49 problems into Lean, refining and verifying each translation.
“We manually translated 49 problems into Lean, refining and verifying each translation.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S4 (based).
Study design and conductnone given
Lean's property-based testing cannot handle a small number of complicated relationships, for which our evaluator returns unknown.
“Lean's property-based testing cannot handle a small number of complicated relationships, for which our evaluator returns unknown.”
Quote in the paperNot a substantial claim
May combine two claims.
Interpretationown data
LLM-based provers are ineffective in the verification domain, as shown in Section 5, making them unreliable for this use case.
“LLM-based provers are ineffective in the verification domain, as shown in Section 5, making them unreliable for this use case.”
Quote in the paperSubstantial claim
May combine two claims.
Interpretationown data
All three tasks pose significant challenges for current LLMs, with constructing Lean proofs that the implementation satisfies the specification being particularly hard and requiring specialized theorem proving capabilities.
“All three tasks pose significant challenges for current LLMs, with constructing Lean proofs that the implementation satisfies the specification being particularly hard and requiring specialized theorem proving capabilities.”
Quote in the paperSubstantial claim
Classified as probably not a substantial claim.
Study design and conductnone given
We manually reviewed and edited the submissions to ensure their correctness.
“In addition, we manually reviewed and edited the submissions to ensure their correctness.”
Quote in the paperSubstantial claim
May combine two claims.
Interpretationown data
All foundational tasks are challenging, especially ProofGen.
“All foundational tasks are challenging, especially ProofGen.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim.
Study design and conductnone given
Generated code is evaluated on unit tests using #guard statements in Lean 4, ensuring the implementation produces correct outputs for given inputs.
“We evaluate generated code on unit tests using #guard statements in Lean 4, ensuring the implementation produces correct outputs for given inputs.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S4 (based).
Interpretationnone given
Using code as specification is uncommon in standard development practices.
“This is likely because using code as specification is uncommon in standard development practices, and our prompts A.3 ask LLMs to focus on constraining code behavior rather than replicating implementation details.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim.
Study design and conductnone given
We made sure that our ground truth code and specifications do not pass these negative tests.
“We made sure that our ground truth code and specifications do not pass these negative tests.”
Quote in the paperSubstantial claim
Classified as probably not a substantial claim.
Study design and conductnone given
Each benchmark instance was manually reviewed by at least two authors, carefully inspecting and editing them to ensure correctness and high quality.
“Each benchmark instance was manually reviewed by at least two authors, carefully inspecting and editing them to ensure correctness and high quality.”
Quote in the paperSubstantial claim
- Rests on an assumption: Manual review by at least two authors ensures correctness and high quality of benchmark instances.
Probably not a substantial claim: may not pass S4 (based).
Interpretationreasoning
Otherwise, it may exploit shortcuts by producing definitionally equivalent code-specification pairs, making the proof task trivial.
“Otherwise, it may exploit shortcuts by producing definitionally equivalent code-specification pairs, making the proof task trivial.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Premisecitation
CloverBench and LiveCodeBench use MIT licenses.
“while both CloverBench [12] and LiveCodeBench [1] use MIT licenses.”
Quote in the paperNot a substantial claim0 of 2 sources checked
- cites [12]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- cites [1]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
May combine two claims.
Study design and conductown data
We added 59 more human-authored Dafny instances from CloverBench, translated into Lean using OpenAI o3-mini with few-shot prompting based on our manual translations, followed by manual inspection and correction.
“These were translated into Lean using OpenAI o3-mini with few-shot prompting based on our manual translations, followed by manual inspection and correction.”
Quote in the paperSubstantial claim0 of 1 sources checked
- cites [12]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Classified as probably not a substantial claim. May combine two claims.
Study design and conductnone given
We mutated each positive test case to construct at least three different negative tests that violate either the pre- or the post-condition, except when the function's output has boolean type, in which case only a single negative test can be created.
“We mutated each positive test case to construct at least three different negative tests that violate either the pre-or the post-condition, except when the function's output has boolean type, in which case only a single negative test can be created.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductnone given
The paper only uses publicly available materials from competitive programming platforms such as LeetCode.
“we only use publicly available materials from competitive programming platforms such as LeetCode.”
Quote in the paperNot a substantial claim
May combine two claims.
Interpretationcitation
VERINA emphasizes simple, standalone tasks that are well-suited for benchmarking but not fully representative of complex real-world verification projects.
“Second, it emphasizes simple, standalone tasks-well-suited for benchmarking but not fully representative of complex real-world verification projects [10,47].”
Quote in the paperNot a substantial claim0 of 2 sources checked
- cites [10]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- cites [47]
  Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Classified as probably not a substantial claim.
Study design and conductnone given
We expanded the set of positive tests to ensure that they achieve full line coverage on the ground truth code.
“Beyond the original test cases, we expanded the set of positive tests to ensure that they achieve full line coverage on the ground truth code.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S4 (based). May combine two claims.
Study design and conductnone given
We employ a meticulous data curation process that combines careful translation, thorough manual review, and automated mechanisms, leading to a rigorous and high-quality benchmark for verifiable code generation.
“We employ a meticulous data curation process that combines careful translation, thorough manual review, and automated mechanisms, leading to a rigorous and high-quality benchmark for verifiable code generation.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductnone given
The paper employs a consistent 2-shot prompting approach across all models and tasks to enhance output format adherence and task understanding.
“We employ a consistent 2-shot prompting approach across all models and tasks to enhance output format adherence and task understanding.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Interpretationown data
This underscores the diversity and varying difficulty levels between VERINA-BASIC and VERINA-ADV.
“This underscores the diversity and varying difficulty levels between VERINA-BASIC and VERINA-ADV.”
Quote in the paperNot a substantial claim
Classified as probably not a substantial claim.
Study design and conductreasoning
We leverage a practical testing-based evaluation framework using our comprehensive test suites.
“To overcome these limitations, we leverage a practical testing-based evaluation framework using our comprehensive test suites, as shown in Figure 3.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S2 (checkable).
Interpretationreasoning
As a result, the model must genuinely demonstrate semantic comprehension of the reference specification and non-trivial reasoning to generate the corresponding implementation.
“As a result, the model must genuinely demonstrate semantic comprehension of the reference specification and non-trivial reasoning to generate the corresponding implementation.”
Quote in the paperNot a substantial claim
May combine two claims.
Study design and conductnone given
The quality assurance process ensures that all ground truth pre-conditions and post-conditions pass positive tests and do not pass negative tests.
“Our quality assurance process in Section 3.2 ensures that all ground truth pre-conditions and post-conditions pass our positive tests and do not pass our negative tests.”
Quote in the paperSubstantial claim
Probably not a substantial claim: may not pass S3 (load-bearing).
Study design and conductnone given
VERINA is licensed under GPL-3.0.
“Our datasets VERINA is licensed under GPL-3.0.”
Quote in the paperNot a substantial claim
Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.
Study design and conductnone given
We leverage 2-shot prompting to enhance output format adherence, with the 2-shot examples excluded from the final benchmark.
“We leverage 2-shot prompting to enhance output format adherence, with the 2-shot examples excluded from the final benchmark.”
Quote in the paperNot a substantial claim
- Rests on an assumption: The 2-shot examples are representative and do not leak benchmark information.
Probably not a substantial claim: may not pass S2 (checkable).
Interpretationreasoning
Very complicated specifications require more comprehensive approaches such as automated theorem provers or LLM-based proof generation.
“very complicated specifications require more comprehensive approaches such as automated theorem provers or LLM-based proof generation”
Quote in the paperNot a substantial claim
May combine two claims.
Interpretationreasoning
The LLM-generated post-condition for the smallest single-digit prime factor task is both unsound (accepts incorrect outputs) and incomplete (rejects valid cases where n = 0).
“This renders the specification both unsound (accepts incorrect outputs) and incomplete (rejects valid cases where n = 0).”
Quote in the paperSubstantial claim
May combine two claims.
Interpretationown data
Iterative refinement with compiler feedback can guide LLMs toward substantially different and correct proof strategies, though it may require many attempts to achieve success.
“This demonstrates how iterative refinement with compiler feedback can guide LLMs toward substantially different and correct proof strategies, though it may require many attempts to achieve success.”
Quote in the paperSubstantial claim
May combine two claims.
Study design and conductown data
The benchmark includes a positive test case where n = 0 and result = 0 and a corresponding negative test case where n = 0 and result = 2 that capture the edge case n = 0.
“We have a positive test case where n = 0 and result = 0 and a corresponding negative test case where n = 0 and result = 2 that capture this edge case.”
Quote in the paperSubstantial claim

73 of 73

The paper relies on this without support.
The test suites are comprehensive enough to serve as a reliable proxy for formal verification of specification soundness and completeness.
“While it cannot formally establish R holds, it remains highly robust in this regard, due to our comprehensive test suite with both positive and negative tests, which achieve full coverage on ground truth code implementations.”
The paper relies on this without support.
The ground truth specifications accurately capture human intent.
“VERINA addresses this by leveraging high-quality ground truth specifications (see Section 3.2) and comprehensive test suites.”
The paper relies on this without support.
Manual review by at least two authors ensures correctness and high quality of benchmark instances.
“Each benchmark instance was manually reviewed by at least two authors, carefully inspecting and editing them to ensure correctness and high quality.”
The paper relies on this without support.
The 2-shot examples are representative and do not leak benchmark information.
“We leverage 2-shot prompting to enhance output format adherence, with the 2-shot examples excluded from the final benchmark.”
The paper relies on this without support.
The model cannot access the code when generating the specification ensures independence.
“When designing VERINA's tasks, we enforce independence-for example, the model cannot access the code when generating the specification.”

5 of 5

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.

Precondition completeness check misclassifies negative tests with valid inputs
Minor
The paper defines negative tests to include cases with valid inputs but invalid outputs. In the cited negative test, k = 2 satisfies the ground-truth precondition k < s.size because the array has five elements. Requiring a generated precondition to reject every negative test would therefore reject a correct precondition and affect the reported specification metric.

1 of 1

Z3: An Efficient SMT Solver
de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595 · cited 1× · see citing works
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
Satisfiability Modulo Theories
Barrett, C. W., Sebastiani, R., Seshia, S., et al. (2009) · Handbook of Satisfiability · doi:10.3233/978-1-58603-929-5-825 · Cited by 1,909 · cited 1×
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
seL4
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al. (2009) · Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles · doi:10.1145/1629575.1629596 · Cited by 1,633 · cited 1× · see citing works
“Second, it emphasizes simple, standalone tasks—well-suited for benchmarking but not fully representative of complex real-world verification projects [10, 47].”
Evaluating Large Language Models Trained on Code
Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. D. O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al. (2021) · arXiv · doi:10.48550/arxiv.2107.03374 · Cited by 1,436 · cited 7× · see citing works
“For each problem instance, we sample 5 responses from each model and calculate pass@1 metrics [3] using these 5 samples to ensure robust evaluation statistics.”
Influential
Satisfiability Modulo Theories
Barrett, C., & Tinelli, C. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_11 · Cited by 1,148 · see citing works
Dafny: An Automatic Program Verifier for Functional Correctness
Leino, K. R. M. (2010) · Lecture Notes in Computer Science · doi:10.1007/978-3-642-17511-4_20 · Cited by 940 · cited 2× · see citing works
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions
Pearce, H., Ahmad, B., Tan, B., Dolan-Gavitt, B., & Karri, R. (2022) · 2022 IEEE Symposium on Security and Privacy (SP) · doi:10.1109/sp46214.2022.9833571 · Cited by 476 · see citing works
Program Synthesis with Large Language Models
Austin, J., Odena, A., Nye, M., Bosma, M., Michalewski, H., Dohan, D., Jiang, E., Cai, C., Terry, M., Le, Q., et al. (2021) · arXiv · doi:10.48550/arxiv.2108.07732 · Cited by 388 · cited 4× · see citing works
“We first consider MBPP-DFY-50 [18], which contains MBPP [24] coding problems paired with human-verified solutions in Dafny.”
Influential
Measuring Mathematical Problem Solving With the MATH Dataset
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., & Steinhardt, J. (2021) · arXiv · doi:10.48550/arxiv.2103.03874 · Cited by 306 · cited 1× · see citing works
“Consistent with established research practices [1, 48], we only use publicly available materials from competitive programming platforms such as LeetCode.”
Self-citation
The Lean 4 Theorem Prover and Programming Language
Moura, L. D., & Ullrich, S. (2021) · Lecture Notes in Computer Science · doi:10.1007/978-3-030-79876-5_37 · Cited by 258 · cited 1× · see citing works
“We format these problems in Lean [19], a general-purpose programming language with a rapidly growing ecosystem and applications in both formal mathematics [20, 21] and verification [22, 23].”
Metrics
Arteaga, I. (2018) · Medicine Anthropology Theory · doi:10.17157/mat.5.4.602 · Cited by 216
The lean mathematical library
Community, T. M. (2020) · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) · doi:10.1145/3372885.3373824 · Cited by 198 · cited 1× · see citing works
“We format these problems in Lean [19], a general-purpose programming language with a rapidly growing ecosystem and applications in both formal mathematics [20, 21] and verification [22, 23].”
Implementing TLS with Verified Cryptographic Security
Bhargavan, K., Cédric Fournet, A., Kohlweiss, M., Pironti, A., & Strub, P.-Y. (2013) · IEEE Symposium on Security and Privacy (S&P) · doi:10.1109/sp.2013.37 · Cited by 177 · cited 1× · see citing works
“Formal verification presents a promising path to establish correctness guarantees in LLM-generated code but has traditionally been limited to safety-critical applications due to high cost [9–11].”
Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program VerificationPreprint
Wen, C., Cao, J.-L., Su, J., et al. (2024) · International Conference on Computer Aided Verification · doi:10.48550/arxiv.2404.00762 · Cited by 154 · cited 3× · see citing works
“Moreover, AutoSpec [27] and SpecGen [28] infer specifications and proofs from human-written code.”
Asleep at the keyboard? Assessing the security of GitHub copilot’s code contributions
Pearce, H., Ahmad, B., Tan, B., Dolan-Gavitt, B., & Karri, R. (2025) · Communications of the ACM · doi:10.1145/3610721 · Cited by 140 · cited 1× · see citing works
“As a result, the generated code often contains bugs, such as functional errors [6] and security vulnerabilities [7].”
MultiPL-E: A Scalable and Polyglot Approach to Benchmarking Neural Code Generation
Cassano, F., Gouwar, J., Nguyen, D., Nguyen, S., Phipps-Costin, L., Pinckney, D., Yee, M.-H., Zi, Y., Anderson, C. J., Feldman, M. Q., et al. (2023) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2023.3267446 · Cited by 109 · cited 1× · see citing works
“• Full code coverage with positive tests : Beyond the original test cases, we expanded the set of positive tests to ensure that they achieve full line coverage on the ground truth code.”
Formal Mathematical Reasoning: A New Frontier in AI
Yang, K., Poesia, G., He, J.-X., Li, W.-D., Lauter, K. E., Chaudhuri, S., & Song, D. (2024) · arXiv.org · doi:10.48550/arxiv.2412.16075 · Cited by 102 · cited 1×
“This approach represents an emerging programming paradigm known as verifiable code generation [12, 13].”
Self-citation
SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
Ma, L., Liu, S., Li, Y., Xie, X., & Bu, L. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00129 · Cited by 98 · cited 3× · see citing works
“Moreover, AutoSpec [27] and SpecGen [28] infer specifications and proofs from human-written code.”
Baldur: Whole-Proof Generation and Repair with Large Language Models
First, E., Rabe, M. N., Ringer, T., & Brun, Y. (2023) · Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering · doi:10.1145/3611643.3616243 · Cited by 94 · cited 1× · see citing works
“…ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust AutoVerus [38] ATP – Rust Laurel [34] ATP – Dafny Pei et al. [33] ATP – Java Baldur [39], Selene [40] ITP – Isabelle Rango [41], PALM [42] ITP – Coq ITPs support constructing proofs with explicit intermediate steps.”
Verus: Verifying Rust Programs using Linear Ghost Types
Lattuada, A., Hance, T., Cho, C., et al. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3586037 · Cited by 93 · cited 1× · see citing works
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
SWE-bench: Can Language Models Resolve Real-World GitHub Issues?
Jimenez, C. E., Yang, J., Wettig, A., Yao, S., Pei, K., Press, O., & Narasimhan, K. (2023) · arXiv · doi:10.48550/arxiv.2310.06770 · Cited by 72 · cited 1× · see citing works
“Large language models (LLMs) have shown strong performance in programming [1–3] and are widely adopted in tools like Cursor and GitHub Copilot to boost developer productivity [4].”
Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification
Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.-C., & Tian, C. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65630-9_16 · Cited by 70 · see citing works
Qwen2.5-Coder Technical Report
Hui, B., Yang, J., Cui, Z., Yang, J., Liu, D., Zhang, L., Liu, T., Zhang, J., Yu, B., Lu, K., et al. (2024) · arXiv · doi:10.48550/arxiv.2409.12186 · Cited by 65 · cited 2× · see citing works
“The costs marked with asterisks include the additional expenses incurred during iterative proof refinement experiments, which required up to 64 refinement attempts per datapoint.”
DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines
Khattab, O., Singhvi, A., Maheshwari, P., Zhang, Z., Santhanam, K., Vardhamanan, S., Haq, S., Sharma, A., Joshi, T. T., Moazam, H., et al. (2023) · arXiv · doi:10.48550/arxiv.2310.03714 · Cited by 60 · cited 1× · see citing works
“We utilize DSPy [49] for structural prompting.”
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Endres, M., Fakhoury, S., Chakraborty, S., & Lahiri, S. K. (2024) · Proceedings of the ACM on software engineering. · doi:10.1145/3660791 · Cited by 57 · cited 1× · see citing works
“…Dafny-Synthesis [18] ATP ✗ Dafny DafnyBench [14] ATP – Dafny miniCodeProps [26] ITP – Lean FVAPPS [17] ITP ✗ Lean T e c hn i qu e s nl2postcond [37] – – Python, Java Clover [12] ATP ✗ Dafny AlphaVerus [15] ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust…”
Aeneas: Rust verification by functional translation
Ho, S., & Protzenko, J. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3547647 · Cited by 51 · cited 1× · see citing works
“These findings underscore the challenges of verifiable code generation and highlight the critical role of V ERINA in advancing the field.”
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Cutler, J. W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Ioannidis, E., Kastner, J., Mamat, A., et al. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3649835 · Cited by 47 · cited 1× · see citing works
“The costs marked with asterisks include the additional expenses incurred during iterative proof refinement experiments, which required up to 64 refinement attempts per datapoint.”
Clover: Closed-Loop Verifiable Code Generation
Sun, C., Sheng, Y., Padon, O., & Barrett, C. (2023) · arXiv · doi:10.48550/arxiv.2310.17807 · Cited by 43 · cited 8×
“This approach represents an emerging programming paradigm known as verifiable code generation [12, 13].”
Influential
Clover: Closed-Loop Verifiable Code Generation
Sun, C., Sheng, Y., Padon, O., & Barrett, C. (2024) · Lecture Notes in Computer Science · doi:10.1007/978-3-031-65112-0_7 · Cited by 43 · see citing works
LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code
Jain, N., Han, K., Gu, A., Li, W.-D., Yan, F., Zhang, T., Wang, S., Solar-Lezama, A., Sen, K., & Stoica, I. (2024) · arXiv · doi:10.48550/arxiv.2403.07974 · Cited by 42 · cited 5× · see citing works
“It draws problems from various sources, including MBPP [18, 24], LiveCodeBench [1], and LeetCode, offering a diverse range of difficulty levels.”
Influential
The Stack: 3 TB of permissively licensed source code
Kocetkov, D., Li, R., Allal, L. B., Li, J., Mou, C., Ferrandis, C. M., Jernite, Y., Mitchell, M., Hughes, S., Wolf, T., et al. (2022) · arXiv · doi:10.48550/arxiv.2211.15533 · Cited by 42 · see citing works
Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models
Wang, Z., Zhou, Z., Song, D., Huang, Y., Chen, S., Ma, L., & Zhang, T. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00180 · Cited by 40 · cited 1× · see citing works
“As a result, the generated code often contains bugs, such as functional errors [6] and security vulnerabilities [7].”
Self-citation
Leveraging automated unit tests for unsupervised code translation
Roziere, B., Zhang, J. M., Charton, F., Harman, M., Synnaeve, G., & Lample, G. (2021) · arXiv · doi:10.48550/arxiv.2110.06773 · Cited by 39 · cited 1× · see citing works
“We created these additional tests both manually and with LLMs.”
Towards AI-Assisted Synthesis of Verified Dafny Methods
Misu, M. R. H., Lopes, C. V., Ma, I., & Noble, J. (2024) · Proceedings of the ACM on Software Engineering · doi:10.1145/3643763 · Cited by 38 · cited 8× · see citing works
“It draws problems from various sources, including MBPP [18, 24], LiveCodeBench [1], and LeetCode, offering a diverse range of difficulty levels.”
Influential
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Mohamed, A., Mascarenhas, T., Khan, H., et al. (2025) · International Conference on Computer Aided Verification · doi:10.48550/arxiv.2505.15796 · Cited by 31 · cited 1×
“Another approach is to convert these relationships into ATP; however, existing tools do not adequately model the necessary Lean features [43].”
Mariposa: Measuring SMT Instability in Automated Program Verification
Zhou, Y., Bosamiya, J., Takashima, Y., et al. (2023) · Formal Methods in Computer-Aided Design · doi:10.34727/2023/isbn.978-3-85448-060-0_26 · Cited by 25 · cited 1×
“However, SMT solvers handle only limited proof domains and behave as black boxes, which can make proofs brittle and hard to debug [35].”
Selene: Pioneering Automated Proof in Software Verification
Zhang, L.-C., Lu, S., & Duan, N. (2024) · Annual Meeting of the Association for Computational Linguistics · doi:10.48550/arxiv.2401.07663 · Cited by 22 · cited 1×
“…ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust AutoVerus [38] ATP – Rust Laurel [34] ATP – Dafny Pei et al. [33] ATP – Java Baldur [39], Selene [40] ITP – Isabelle Rango [41], PALM [42] ITP – Coq ITPs support constructing proofs with explicit intermediate steps.”
AutoVerus: Automated Proof Generation for Rust Code
Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S., et al. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763174 · Cited by 20 · cited 1× · see citing works
“…– Python, Java Clover [12] ATP ✗ Dafny AlphaVerus [15] ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust AutoVerus [38] ATP – Rust Laurel [34] ATP – Dafny Pei et al. [33] ATP – Java Baldur [39], Selene [40] ITP – Isabelle Rango [41], PALM [42] ITP – Coq ITPs…”
Proof Automation with Large Language Models
Lu, M., Delaware, B., & Zhang, T. (2024) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3691620.3695521 · Cited by 17 · cited 1× · see citing works
“…ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust AutoVerus [38] ATP – Rust Laurel [34] ATP – Dafny Pei et al. [33] ATP – Java Baldur [39], Selene [40] ITP – Isabelle Rango [41], PALM [42] ITP – Coq ITPs support constructing proofs with explicit intermediate steps.”
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Thompson, K., Saavedra, N., Carrott, P., Fisher, K. D., Sanchez-Stern, A., Brun, Y., Ferreira, J. F., Lerner, S., & First, E. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00161 · Cited by 14 · cited 1× · see citing works
“…ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++ SpecGen [28] ATP ✗ Java SAFE [16] ATP ✗ Rust AutoVerus [38] ATP – Rust Laurel [34] ATP – Dafny Pei et al. [33] ATP – Java Baldur [39], Selene [40] ITP – Isabelle Rango [41], PALM [42] ITP – Coq ITPs support constructing proofs with explicit intermediate steps.”
Laurel: Unblocking Automated Verification with Large Language Models
Mugnier, E., Gonzalez, E. A., Polikarpova, N., Jhala, R., & Yuanyuan, Z. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720499 · Cited by 14 · cited 2× · see citing works
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
Verified Foundations for Differential Privacy
de Medeiros, M., Naveed, M., Lepoint, T., et al. (2024) · IACR Cryptology ePrint Archive · doi:10.1145/3729294 · Cited by 14
Tabled Typeclass ResolutionPreprint
Selsam, D., Ullrich, S., & de Moura, L. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2001.04301 · Cited by 11 · cited 1× · see citing works
“For many cases, e.g., the specification in Figure 1, Lean can automatically determine if R ′ holds [44] and we return the corresponding result.”
Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
Rego, M., Fan, W., Hu, X., et al. (2024) · arXiv.org · doi:10.48550/arxiv.2411.02318 · Cited by 10 · cited 1×
“We utilize the standard pass@ k metric [25] with our comprehensive test suites to evaluate code generation.”
DafnyBench: A Benchmark for Formal Software Verification
Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., & Tegmark, M. (2024) · arXiv · doi:10.48550/arxiv.2406.08467 · Cited by 6 · cited 3× · see citing works
“Existing benchmarks, as listed in Table 1 and detailed in Section 2, fall short as they lack comprehensive support for all three tasks [14–16], quality control [17], robust metrics [18], or a modular design [12].”
Untitled work
(2025) · doi:10.1109/llm4code66737.2025.00014 · Cited by 6 · cited 4× · see citing works
“Existing benchmarks, as listed in Table 1 and detailed in Section 2, fall short as they lack comprehensive support for all three tasks [14–16], quality control [17], robust metrics [18], or a modular design [12].”
Influential
DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
Ren, Z. Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., et al. (2025) · arXiv · doi:10.48550/arxiv.2504.21801 · Cited by 4 · cited 1×
“Our collection and use of these problems is strictly for academic research purposes, and V ERINA involves no model training or fine-tuning processes.”
An In-Context Learning Agent for Formal Theorem-ProvingPreprint
Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., & Chaudhuri, S. (2023) · arXiv (Cornell University) · doi:10.48550/arxiv.2310.04353 · Cited by 4 · cited 1× · see citing works
“Our collection and use of these problems is strictly for academic research purposes, and V ERINA involves no model training or fine-tuning processes.”
AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
Aggarwal, P., Parno, B., & Welleck, S. (2024) · arXiv · doi:10.48550/arxiv.2412.06176 · Cited by 4 · cited 2× · see citing works
“This aligns with tasks explored in FVAPPS [17] and AlphaVerus [15].”
miniCodeProps: a Minimal Benchmark for Proving Code Properties
Lohn, E., & Welleck, S. (2024) · arXiv · doi:10.48550/arxiv.2406.11915 · Cited by 2 · cited 3×
“B e n c h m a r k s HumanEval [3], MBPP [24] – – Python Dafny-Synthesis [18] ATP ✗ Dafny DafnyBench [14] ATP – Dafny miniCodeProps [26] ITP – Lean FVAPPS [17] ITP ✗ Lean T e c hn i qu e s nl2postcond [37] – – Python, Java Clover [12] ATP ✗ Dafny AlphaVerus [15] ATP ✗ Rust AutoSpec [27] ATP ✗ C/C++…”
Automated Proof Generation for Rust Code via Self-Evolution
Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., et al. (2024) · arXiv · doi:10.48550/arxiv.2410.15756 · Cited by 1 · cited 3×
“Existing benchmarks, as listed in Table 1 and detailed in Section 2, fall short as they lack comprehensive support for all three tasks [14–16], quality control [17], robust metrics [18], or a modular design [12].”
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionPreprint
Lin, Y., Tang, S., Lyu, B., Yang, Z., Chung, J.-H., Zhao, H., Jiang, L., Geng, Y., Ge, J., Sun, J., et al. (2025) · arXiv (Cornell University) · doi:10.48550/arxiv.2508.03613 · cited 3×
“Our collection and use of these problems is strictly for academic research purposes, and V ERINA involves no model training or fine-tuning processes.”
Self-citation
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Thakur, A., Lee, J., Tsoukalas, G., Sistla, M., Zhao, M., Zetzsche, S., Durrett, G., Yue, Y., & Chaudhuri, S. (2025) · arXiv · doi:10.48550/arxiv.2505.13938
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
Dougherty, Q., & Mehta, R. (2025) · arXiv · doi:10.48550/arxiv.2502.05714
Selene: Pioneering Automated Proof in Software Verification
Zhang, L., Lu, S., & Duan, N. (2024) · Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · doi:10.18653/v1/2024.acl-long.98

Flagged first, then by citations

13 of the 68 references couldn’t be matched to a known paper.

Research works printed but not linked: 3

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Symposium on Operating Systems Design and Implementation (OSDI), 2016. 1
Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In International Conference on Machine Learning (ICML), 2023. 2, 3
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformal- ization: towards a faithful metric and a dependency retrieval-based approach. In International Conference on Learning Representations (ICLR), 2025. 8

Sorted by citations

Large Language Model Reasoning Failures
Song, P., Han, P., & Goodman, N. (2026) · arXiv · doi:10.48550/arxiv.2602.06176 · Cited by 3 · see citing works
A benchmark for vericoding: formally verified program synthesis
Bursuc, S., Ehrenborg, T., Lin, S., Astefanoaei, L., Chiosa, I. E., Kukovec, J., Singh, A., Butterley, O., Bizid, A., Dougherty, Q., et al. (2025) · arXiv · doi:10.48550/arxiv.2509.22908 · Cited by 1 · see citing works
“Formal verification or vericoding benchmarks such as DafnyBench (Loughridge et al., 2025) for Dafny, VerifiedCogen (JetBrains-Research, 2025) for Verus, and Verina (Ye et al., 2025) and Clever (Thakur et al., 2025) for Lean.”
Influential
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Bayazıt, B., Li, Y., & Si, X. (2025) · ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL) · doi:10.1145/3759425.3763391 · Cited by 1 · see citing works
“Outside Rocq Prover, there are many benchmarks for other proof assistants or formal-method tools, such as Dafny-Bench [53], LeanDojo [96], miniCodeProps [52], FVAPPS [22], VerifyThisBench [21], Verina [97], etc. Proof automation.”
Code as Agent Harness
Ning, X., Tieu, K., Fu, D., Wei, T., Li, Z., Bei, Y., Zou, J., Ai, M., Liu, Z., Li, T.-W., et al. (2026) · arXiv · doi:10.48550/arxiv.2605.18747
Self-citation
Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean
Gladshtein, V., Kurin, V., Feng, Y., et al. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-32526-6_11
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
Ioannidis, E., Swamy, N., Ebner, G., Philipose, M., & Ramananandro, T. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3828709
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
Zhao, H., Yang, Z., Li, J., He, D., Li, Z., Jin, C., Veeravalli, V. V., Gupta, A., & Arora, S. (2026) · arXiv · doi:10.48550/arxiv.2602.09464

Authors: Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., & Song, D.
Affiliations: University of California, Berkeley (US)
ORCID: He, Jingxuan
Yang, Kaiyu
Venue: arXiv
Publisher: arXiv
Published: 2025
ISSN: 2331-8422 (ISSN-L)
DOI: 10.48550/arxiv.2505.23135
arXiv: 2505.23135
OpenAlex: W4416609154
Cited by: 3
References: 68
Citations by year: 2026: 2 · 2025: 1
Type: posted content
Language: en
Open access: green
arxiv.org
Licence: cc-by-sa
creativecommons.org/licenses/by-sa/4.0/legalcode
Locations: arXiv (Cornell University) (submittedVersion, cc-by-sa)
arXiv (Cornell University)
Topics: Physical Sciences › Computer Science › Information Systems › Software Engineering Research
Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords: benchmarking, large language models, formal verification, lean manufacturing, proof generation, program correctness

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.

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

VERINA: Benchmarking Verifiable Code Generation

Abstract

AI snapshot

TL;DR

Key findings

Methods

Limitations

Integrity signals

Claims the paper makes

Self-check

Cites

Cited by

Record

About these checks