A Benchmark for Vericoding: Formally Verified Program Synthesis

## Abstract

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 in this GitHub repo . 1 1 1 Beneficial AI Foundation 1 2 2 footnotetext: Massachusetts Institute of Technology

## 1 Introduction

Rapid AI progress has popularized vibe coding, which generates computer programs from natural language descriptions.
For example, Google has reported that over 30% of its software is created this way (Google Earnings Call,). Unfortunately, the resulting code can be buggy, and traditional bug hunting with test cases can typically only demonstrate
the presence and not the absence of bugs,
since there are too many test cases to try them all.
For example, major code-testing efforts failed to prevent bugs causing an Ariane-V rocket explosion (Ariane 5 Failure,)
and an embarrassing security vulnerability
in the Bash shell (Shellshock Bug,) that was built into the Unix operating system for 25 years before being discovered. The 2024 CrowdStrike outage disrupted 8.5 million devices globally, harming airlines, hospitals, banking, broadcasting, emergency services (CrowdStrike Outage,).

Fortunately, rigorous correctness guarantees can be created via formal verification, by generating a machine-checkable proof that code meets its human-written specifications. 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.

This makes it timely to test whether AI can help, either by verifying existing code or by writing new formally verifiable code from scratch based on its specification,
which we term vericoding. 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. It is easy to imagine formal verification being simply a built-in final step of future compilers, which discover code problems and
attempt to fix them automatically. One can also imagine a future where humans do not need to write programs, only specs.

This optimistic premise is based on the close analogy with automated theorem proving, where AI produces formal proofs not about code but about mathematical theorems. 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). In August 2025, Seed-Prover
achieved over 50% on PutnamBench (Chen et al., 2025), proved 78.1% of formalized past mathematics olympiad problems, and scored 99.6%
on the MiniF2F benchmark (up from a 50% SOTA mid 2024). Together with the Seed-Geometry engine, the models solved 5 of 6 problems at IMO 2025.

Unfortunately, formal verification sorely lacks correspondingly large benchmarks: the largest of their kind contain fewer than $10^{3}$ examples.
There is room for expanding not only their size and diversity, but also their level of difficulty:
Many examples are limited to single-function programs, and sometimes the formal specification for a program directly
repeats an implementation of the algorithm.
To support automation of formal verification and vericoding, the goal of the present paper is to provide such a benchmark expansion, by assembling and testing a suite of formal specifications for Lean (Moura & Ullrich, 2021), Rust/Verus (Lattuada et al., 2024) and Dafny (Leino, 2010).

The rest of this paper is organized as follows.
We summarize related work in Section 2, and describe our benchmark construction in Section 3, outlining how vericoding sources were assembled or translated from natural language documentation, vibe coding datasets and verification benchmarks. In Section 4, we quantify the ability of current LLMs to solve vericoding tasks. Special attention is given to Lean tasks, because of recent successes in AI-assisted theorem proving. For example, we explore specifications expressed as Hoare triples using a new *mvcgen* feature. We summarize our conclusions in Section 5 and provide further technical details of our translation and vericoding approaches in the Appendix in the supplementary material.

## 2 Related Work

Over the past two years, there has been increased interest in constructing new benchmarks for verification (proofs from formal specifications and implementations) and vericoding (implementations and proofs from formal specifications), as seen in Table [1](https://arxiv.org/html/2509.22908v1#S2.T1), much work remains. There is significant variation in the types of verification and vibe coding tasks. VerifyThisBench (Deng et al., 2025), for example, generates specs, implementations and proofs jointly from natural language descriptions. Meanwhile, VeriBench (Miranda et al., 2025) takes Python code and documentation, and generates implementations, specs and unit tests in Lean to be proved by the LLM. A novel form of vibe coding comes from the FVAPPS (Dougherty & Mehta, 2025) benchmark which contains formal specs generated from natural language descriptions. For code synthesis, the LLM is given the descriptions and the formal specs, and specs and unit tests are employed to provide some formal correctness guarantees. Meanwhile, the field of AI control (Greenblatt et al., 2024) checks AI-produced code for correctness and safety
using techniques such as oversight by weaker LLMs, but this does not produce formal guarantees.

In vericoding, no natural language descriptions are provided to the LLM for code generation. In benchmarks such as CLEVER (Thakur et al., 2025) and VERINA (Ye et al., 2025), the tasks include formal spec generation from documentation, in addition to formal and proof generation. Both benchmarks also require the Lean implementation to be synthesized *before* constructing a proof of its correctness. We acknowledge that spec generation is an important problem, but focus on the task of generating implementations and formal proofs in this work. We also let the LLM generate the implementation and the proof jointly — over several iterations, the model is allowed to change the implementation to make the proof easier or correct mistakes.

The challenge of constructing large coding benchmarks lies in gathering a large base of problems, formatting them and checking them for quality. DafnyBench (Loughridge et al., 2025) builds this base from existing benchmarks such as Clover and DafnySynthesis, and from GitHub scrapes. Large language models (LLMs) and other LLMs have facilitated this. FVAPPS (Dougherty & Mehta, 2025) uses LLMs to translate Python tasks from the APPS benchmark to Lean, and to format the translations. AlphaVerus (Aggarwal et al., 2024) goes further with a self-improving framework that iteratively translates programs from Dafny to Verus and leverages feedback from the verifier. In our work, we instead use LLMs out of the box, using them not just for translation, but also for critiquing the translations and for fixing errors in them.

**Table 1: Recent benchmarks for theorem proving, verification, vibe coding and vericoding. Verification and vericoding benchmarks are two orders of magnitude smaller than those for theorem proving and vibe coding. We list only benchmarks for Dafny, Verus and Lean. Notable benchmarks in other languages are SV-COMP (Beyer & Strejček, 2025) and SyGuS (Alur et al., 2018) in C and Java, and FVELER (Lin et al., 2024) and AFP (Archive of Formal Proofs,) in Isabelle. In comparison, we have 12504 tasks of which 6174 are new or translated from other benchmarks.**
| Task | Benchmark | Language | Size |
| --- | --- | --- | --- |
| Thm proving | PutnamBench (Tsoukalas et al., 2024) | Lean, Isabelle, Coq | 1709 |
| Thm proving | FormalMATH (Yu et al., 2025) | Lean | 5560 |
| Thm proving | LeanDojo (Yang et al., 2023) | Lean | 98734 |
| Thm proving | LISA (Jiang et al., 2021) | Isabelle | 183000 |
| Verification | VeriBench (Miranda et al., 2025) | Lean | 113 |
| Verification | Verus-Bench (Yang et al., 2025) | Verus | 150 |
| Verification | Verified Cogen (JetBrains-Research, 2025) | Verus (among others) | 223 |
| Verification | VerifyThisBench (Deng et al., 2025) | Dafny, Why3, etc. | 481 |
| Verification | DafnyBench (Loughridge et al., 2025) | Dafny | 782 |
| Vibe coding | HumanEval (Chen et al., 2021) | Python | 163 |
| Vibe coding | FVAPPS (Dougherty & Mehta, 2025) | Lean | 4715 |
| Vibe coding | APPS (Hendrycks et al., 2021) | Python | 10000 |
| Vibe coding | CodeContests (Li et al., 2022) | Mixed | 13610 |
| Vibe coding | HumanEval-XL (Peng et al., 2024) | Mixed | 22080 |
| Vericoding | CLEVER (Thakur et al., 2025) | Lean | 161 |
| Vericoding | VERINA (Ye et al., 2025) | Lean | 189 |

## 3 Benchmark Construction

We are primarily interested in constructing a benchmark for two kinds of provers: automated theorem provers (ATPs) such as Dafny and Verus, which use SMT solvers to automatically discharge verification conditions, and interactive theorem provers (ITPs) such as Lean, which use tactics to build proofs. We begin by curating some original sources, such as HumanEval, Clever, Verina, APPS, and Numpy documentation. The original sources are then translated into other languages. Lastly, the translations are compiled, parsed into different sections, and quality-checked. We include tasks with specs that are incomplete, inconsistent, or non-compilable, because spec repair is an essential part of the formal verification workflow. Further details and scripts used in our construction can be found in the Appendix and in the supplementary material.

**Table 2: Number of tasks for each language and source. Originals are in bold, and translations are not. The $*$ indicates new tasks. $X\!:\!Y$ indicates that $X$ tasks were generated during translation, and $Y$ tasks remained after compiling, formatting and quality checks. We use only the latter tasks for our experiments. We release also the problematic tasks in case there is interest to use them for other purposes, such as spec repair. The task IDs are of the form XYdddd where X indicates the language (Dafny, Lean, Verus), Y refers to the source (see the Ref column in the table) and dddd is a four-digit zero-padded number starting from 0000.**
| Source | Ref | Dafny | Verus | Lean | Total |
| --- | --- | --- | --- | --- | --- |
| APPS (Test) | A | 883 : 677 * | 677 : 536 * | 677 : 676 * | 2237 : 1889 |
| $\mathsf{DafnyBench}$ | D | 929 : 443 | 442 : 440 * | 440 : 440 * | 1811 : 1323 |
| NumpyTriple | T | 603 : 603 * | 603 : 581 * | 666 : 603 * | 1872 : 1787 |
| VerifiedCogen | J | 172 : 172 * | 172 : 172 | 172 : 172 * | 516 : 516 |
| Verina | V | 157 : 157 * | 157 : 156 * | 189 : 189 | 503 : 502 |
| Bignum | B | 62 : 62 * | 62 : 62 * | 62 : 62 * | 186 : 186 |
| NumpySimple | S | 59 : 58 * | 59 : 58 * | 59 : 59 * | 177 : 175 |
| HumanEval | H | 164 : 162 | 162 : 161 * | 161 : 161^1 | 487 : 484 |
| FVAPPS | F |  |  | 4715 : 4006 | 4715 : 4006 |
| Total |  | 3029 : 2334 | 2334 : 2166 | 7141 : 6368 | 12504 : 10868 |
|  |  | 1936 : 1729 * | 2162 : 1994 * | 2076 : 2012 * | 6174 : 5735 * |

### 3.1 Vericoding definitions

A *documentation* is a collection of natural language text that describes the *intent* (intended behavior) and optionally the *pseudocode* (prescribed algorithm) of some program. A *specification* (or *spec*) is a representation of the intent in a formal language. It contains both the function *signature* (name, input types and output types) and the *conditions* (e.g., preconditions, postconditions) that the functions must satisfy. *Code* refers to a program implementation that can be executed or checked. A *proof* is a formal demonstration of the correctness of an implementation with respect to some specification. Specifications and code may refer to an external *context* that contains the definitions of the objects used. These can be boolean predicates, mathematical functions, data structures, and algorithms. The context may be defined within the same file or imported from external files. In ITPs, the specification signature and its implementation are grouped to form a *definition*. The implementation can be unfolded from the definition as needed, e.g. for the proof. The specification conditions and their proof are also paired to form a *theorem* where the proof details are opaque and cannot be unfolded from the theorem. By making proofs opaque, theorems can only depend on the conditions of other theorems and not on their proofs. In ATPs, the specification signature and its conditions are grouped together, while the implementation and proof interleave to form the (proof-carrying) code.

A *vericoding task* consists of the context and the spec, and optionally the documentation, which are passed to the LLM model. A *vericoding solution* contains the implementation, the proof, as well as any additional context that is needed, often in the form of imports, *helper* functions, and helper lemmas. As shown in [Figure 1](https://arxiv.org/html/2509.22908v1#S3.F1), we use tags to indicate different components of a task or solution file: documentation, spec, code, preamble, postamble and helper contexts. Most of the tasks –such as those from Verina, Clever, DafnyBench, and Numpy Triple– require vericoding for exactly one function. Other tasks, such as those from FVAPPS, require implementations of several functions and proofs that they work together in the desired way. For example, LF0007 (a lead-up to LF0023) asks for the ins and pop operations on a heap, and a proof that popping the elements off a heap produces a sorted list. Some Lean tasks include unit tests, which are put in the postamble. Examples of these tests can be found in FVAPPS, Verina, and Clever. Unit tests are not given to the LLM for vericoding, as the LLM can otherwise easily design implementations that pass all unit tests. They are instead applied to the implementation as an additional layer of checks after vericoding is completed.

Figure: Figure 1: Examples of vericoding tasks. We use *vc* tags for elements introduced in [Section 3.1](https://arxiv.org/html/2509.22908v1#S3.SS1).

### 3.2 Original sources and task generation

We generate vericoding tasks from three types of original sources (see bold text in Table [2](https://arxiv.org/html/2509.22908v1#S3.T2)) :

- 1.
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.
- 2.
Vibe coding benchmarks such as APPS (Hendrycks et al., 2021), FVAPPS (Dougherty & Mehta, 2025) and HumanEval (Chen et al., 2021).
- 3.
Documentations of mathematical function libraries such as Numpy (Harris et al., 2020, v2.3) and BigNum (Polubelova, 2022).

These sources often contain proposed implementations and sometimes proofs in addition to formal or informal specifications for each task. To obtain a vericoding task, we delete the implementation of the main coding task and all helper lemmas and proofs, and replace them with holes (e.g. sorry). For the vibe coding and documentation sources, we also perform autoformalization to obtain a formal spec for each task. We elaborate on our process for each source in Appendix [1.1](https://arxiv.org/html/2509.22908v1#A1.SS1).

### 3.3 Spec translations and validation

Figure: Figure 2: LLM-based translation of vericoding specifications.

To expand task coverage across languages, we translate tasks between Dafny, Verus, and Lean(^3^33With the exception of (FV)Apps/Humaneval where the source language is in Python. The translator from Python to Dafny extends on the one in Figure [2](https://arxiv.org/html/2509.22908v1#S3.F2) with a generator-vs-judge game.). Figure [2](https://arxiv.org/html/2509.22908v1#S3.F2) shows our LLM-based translation algorithm, which attempts up to $k$ iterations to produce verified translations. The process uses *structured processing* of tagged specifications (vc-description, vc-preamble, vc-spec, vc-code, vc-postamble) and a *conversational repair loop* that maintains translation history to learn from verification feedback. Since we translate only specifications (not implementations), we expect higher translation success rates as specifications are typically easier to translate than complete implementations. Translation counts are shown in Table [2](https://arxiv.org/html/2509.22908v1#S3.T2) (plaintext).

Validation: We validated translated specifications through two approaches. First, we used the “LLM as a judge”, asking it to compare each translation against its tagged source to verify faithful preservation of preconditions, postconditions, and invariants. This catches attempts to trivialize verification—such as replacing complex postconditions with ensures true or substituting function bodies with default values. Second, through manual inspection, we picked a random sample of translated specifications to inspect for correctness. We discovered that a handful of specifications admitted trivial solutions, which were due to lossy LLM transpilation or due to incomplete human-authored specifications that failed to fully capture their natural-language descriptions.

Quality assessment: We assess benchmark quality using a scoring framework that penalizes language-specific issues and near-duplicates. The quality score per file in a benchmark is $1-(\sum_{i}w_{i}\times n_{i})$ where $w_{i}$ is the normalized weight for issue type $i$ (weights sum to 1.0) and $n_{i}$ is the number of issue types $i$ in that file.
Near-duplicate detection uses sentence transformers (Reimers & Gurevych, 2019) with FAISS indexing (Johnson et al., 2017) to compare normalized problem descriptions and specifications. Typical issues include Verus specs which return a default value instead of having an implementation (see Figure [7](https://arxiv.org/html/2509.22908v1#A1.F7)(a) in the Appendix for an example).

All quality metrics, scores, and detected issues are embedded as metadata in the benchmark JSONL files. A summary of the quality metrics is shown in Table [5](https://arxiv.org/html/2509.22908v1#A1.T5) in the Appendix.

## 4 Vericoding Experiments

Figure: Figure 3: Vericoding process using an LLM model $\mathcal{M}$ for vericoding tasks $\mathcal{S}$ and language $\mathcal{L}$

We quantify the vericoding success rate for LLMs such as GPT and Claude straight out of the box, without special techniques such as reinforcement learning or fine-tuning. Our experimental pipeline is simple: we present to the LLM a prompt that is annotated to indicate the context, the problem spec, as well as different holes (e.g. sorry’s) that require input from the LLM model. The model responds with blocks generated for each of the holes. The generated blocks are *validated* by checking for cheating patterns, and inserted into the task file template. The file is then *verified* with the proof checker. If both validation and verification pass, the LLM is deemed to have successfully completed the task. Otherwise, the error messages are passed to the LLM for correction. We allow only a fixed number of such iterations before deciding that the LLM has failed. This process is described more precisely in [Figure 3](https://arxiv.org/html/2509.22908v1#S4.F3). The validation tests are specific for each proof language. They depend on corresponding compile options, syntax and programming patterns. 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.

Prompts and hyperparameters: We have two prompt templates for each language, listed in Appendix [1.3](https://arxiv.org/html/2509.22908v1#A1.SS3): one for code and proof generation and one for fixing verification errors in previously generated files. We informally explored prompting variations, but did not optimize the prompts fully. The Verus prompt might benefit from examples of common lemmas in vstd. For Dafny/Verus, we gave sample syntax in the prompt. Each LLM had 5 attempts per task, except 10 attempts on the challenging BigNum dataset. In comparison, Harmonic used half a million CPUs to run Lean for its IMO work (Harmonic, 2025).

LLM cheating detection: Our block validation script systematically detects potential LLM cheating patterns that could bypass the proof checker, possibly by changing the goals. These include : (1) Using assume(false) or sorry to disable the proof checker. We can instruct the proof checker to reject such proofs. (2) Changing postconditions in the spec to ensures true to make it trivial to prove. We can block the LLM from altering the specs. (3) Implementation leakage from the spec. We use ghost functions in Dafny/Verus to partly mitigate this. There will typically be some level of implementation leakage from the specs–if not the full implementation, then at least the spirit of it. Indeed, we expect LLMs to do so, so the onus is on spec writers to create good specs (see, e.g., the CLEVER benchmark). (4) We anticipated a cunning form of cheating where the LLM begins a comment section in one block and closes the comment section in another, effectively erasing any intermediate task spec through this trick. Thankfully, this did not happen.

Manual inspection: 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. The reports, detailed in the supplementary material, show language-specific patterns: Dafny exhibited no issues (except for redundant lemmas), with LLMs correctly giving trivial solutions when the specs were weak. Verus showed many weak specs due to spec translation issues, e.g. deviations from the original BigNum specs in Dafny. Lean displayed occasional redundant lemma additions during vericoding, and had some weak specs from the original sources. Across Dafny, Verus and Lean, conditioned on vericoding success, roughly 9% of the specs were too weak and another 15% had poor translations. Note that these problematic specs still make perfectly valid vericoding tasks, just different tasks than originally intended. No further cheating was discovered, other than those which were caught by our validation checks.

### 4.1 Vericoding results

Table [3](https://arxiv.org/html/2509.22908v1#S4.T3) shows that LLM vericoding worked best on Dafny (82.2%), followed by Verus (44.2%) and Lean (26.8%). Claude-Opus- 4.1 excelled at Dafny, while GPT-5 led on Verus and Lean. The “model union” numbers denote the fraction solved by at least one of the LLMs.

Verus success rates are probably lower due to several factors: unlike Dafny’s uniform mathematical types, Verus distinguishes between ghost types (for specifications) and Rust native types (for execution), requiring verification of machine-level complexities such as overflow handling. Additionally, LLM translations often fail to systematically map between these type systems, and Verus is a newer, lower-resource language than Dafny.

Lean’s lower success probably stems mostly from LLMs being trained primarily on mathematical theorem proving rather than code verification. The Lean prompt might benefit from examples of how to use new tactics such as grind and canonical. ITPs and ATPs will
also require different strategies for exploiting LLMs: A human writing Lean gets constant feedback about the proof state, while our scaffolding only told the LLM what the proof state was 5 times per example.

We have separated FVAPPS into Row A of Table [3](https://arxiv.org/html/2509.22908v1#S4.T3) because the specs are weaker and allow for more trivial solutions. We did not apply the unit tests associated to the tasks in these experiments. Here, GPT-5 is again seen to perform best.

Verification alone: We use the original dataset from Loughridge et al. (2025) with 782 tasks and its original prompts to gauge how much the LLMs have improved on verification.
Table [3](https://arxiv.org/html/2509.22908v1#S4.T3) shows the success rates (sample sizes in parentheses) for different LLMs, revealing rapid progress:
The June 2024 state-of-the-art of 68% with Opus-3 has
now risen to 89% with Opus-4.1 and 96% for the model union.
See Appendix
[1.6](https://arxiv.org/html/2509.22908v1#A1.SS6) for more details.

Hoare triples in Lean: The model union achieved 7.6% success on our novel Numpy-Triple benchmark, which is below the language average of 26.8%. This is likely due to the mvcgen feature being new. We expect the success rate to improve significantly over the next two years when newer LLMs are trained on datasets that use this feature and as SMT-solver-based tactics in Lean become more proficient at tackling the proof obligations.

Spec and vibe coding: In addition to formal specifications, several of our source benchmarks contain informal descriptions of vericoding tasks. One of these is Verina, for which we perform a separate set of experiments including the informal descriptions in the LLM prompt. The aim is to test their effect on vericoding performance. We find that including the ”vibe” information provides no statistically significant performance improvement (indeed, the results seen to be slightly worse on average), so we decided not to extended this experiment to our full benchmark, and plan to study this more extensively in future work.

Improvements from ensemble methods:
Results from taking the union of successful attempts from different models can be found in Table [3](https://arxiv.org/html/2509.22908v1#S4.T3). This potentially suggests that in the future, vericoding tasks should be decomposed into smaller parallel tasks that can be tackled by different models. To make this like a mixture of experts (MoE) strategy in advanced language models (Jiang et al., 2024), we would need to implement a router model (perhaps just a pre-deep-learning bag-of-words model) that decides which LLM will attempt a problem.

### 4.2 Parameters influencing vericoding difficulty

We investigate three different parameters that one may expect to impact vericoding complexity: *spec length* (the number of characters in the spec source code), *solution length* (the number of characters in the LLM’s solution), and *spec ratio* (code length divided by spec length).
Note that an LLM’s solution may or may not be code that satisfies the spec or even parses in its target language, since not all solutions are correct.

Spec length depends on the number of preconditions, postconditions, and helper definitions. More preconditions ease verification by providing assumptions, while more postconditions increase difficulty by requiring additional proofs. Helper definitions create interdependent proof obligations that are harder to solve.

We find that LLMs easily generate implementations (consistent with vibe coding success), but struggle more with proofs — adding invariants/assertions for ATPs or choosing tactics for ITPs. Our results, shown in
Figure [4](https://arxiv.org/html/2509.22908v1#S4.F4), exclude all cases where the LLM fails to propose an implementation.

Figure: Figure 4: Vericoding success as a function of task spec length (top row), generated code length (middle row) and spec ratio (bottom row) which is the code length divided by the spec length. sorted by size
Refer to caption: x1.png

Figure [4](https://arxiv.org/html/2509.22908v1#S4.F4) shows the relation between vericoding success and the various parameters.
Spec length is the weakest predictor of vericoding complexity, presumably because simple problems can have lengthy solutions (e.g., Fermat’s Last Theorem). Additionally, longer specs often contain helper functions that do not require vericoding, unlike additional postconditions which increase difficulty. Solution length shows a clearer trend: longer implementations are more likely incorrect, similar to human coding where more code increases error probability. With finite iterations per task, shorter implementations allow better use of each iteration. Spec ratio trends fall between these patterns, following solution length trends more closely.

**Table 3: Vericoding results**
| NumPyS<br>NumPy3<br>DafnyBench<br>HumanEval<br>Verina<br>BigNum<br>VerifCogen<br>APPStest<br>Totals $\downarrow$<br>Dafny<br>58 tasks<br>430 tasks<br>443 tasks<br>162 tasks<br>157 tasks<br>62 tasks<br>172 tasks<br>677 tasks<br>2161 tasks<br>claude-opus-4.1<br>60.3%<br>64.9%<br>67.0%<br>71.6%<br>73.2%<br>14.5%<br>90.7%<br>66.6%<br>67.5%<br>gpt-5-mini<br>67.2%<br>56.3%<br>64.1%<br>71.6%<br>73.9%<br>25.8%<br>85.5%<br>71.6%<br>66.9%<br>gpt-5<br>65.5%<br>56.3%<br>63.9%<br>72.2%<br>76.4%<br>19.4%<br>86.6%<br>69.1%<br>66.1%<br>claude-sonnet-4<br>65.5%<br>69.3%<br>61.2%<br>72.8%<br>72.0%<br>8.1%<br>84.3%<br>60.3%<br>64.6%<br>gemini-2.5-pro<br>63.8%<br>60.2%<br>58.2%<br>69.1%<br>66.9%<br>6.5%<br>79.7%<br>40.8%<br>55.0%<br>grok-code<br>48.3%<br>47.0%<br>52.8%<br>57.4%<br>63.1%<br>3.2%<br>75.6%<br>52.9%<br>53.0%<br>glm-4.5<br>50.0%<br>41.4%<br>20.3%<br>50.0%<br>51.0%<br>4.8%<br>67.4%<br>48.7%<br>42.0%<br>gemini-2.5-flash<br>48.3%<br>34.4%<br>36.3%<br>42.6%<br>45.9%<br>0.0%<br>57.0%<br>36.9%<br>38.2%<br>deepseek-chat-v3.1<br>39.7%<br>43.0%<br>30.2%<br>45.1%<br>46.5%<br>3.2%<br>50.0%<br>30.6%<br>36.2%<br>model union<br>75.9%<br>77.9%<br>71.9%<br>93.2%<br>87.3%<br>48.4%<br>95.9%<br>83.0%<br>82.2%<br>Verus<br>58 tasks<br>581 tasks<br>443 tasks<br>161 tasks<br>156 tasks<br>62 tasks<br>172 tasks<br>536 tasks<br>2166 tasks<br>gpt-5<br>18.9%<br>47.5%<br>18.3%<br>15.5%<br>30.7%<br>3.2%<br>49.4%<br>26.5%<br>30.9%<br>claude-opus-4.1<br>18.9%<br>29.7%<br>19.2%<br>9.9%<br>26.2%<br>1.6%<br>63.4%<br>18.1%<br>24.6%<br>gemini-2.5-pro<br>34.5%<br>31.5%<br>19.7%<br>9.3%<br>25.6%<br>1.6%<br>52.9%<br>16.0%<br>24.1%<br>claude-sonnet-4<br>20.7%<br>22.0%<br>19.0%<br>5.6%<br>27.5%<br>1.6%<br>48.2%<br>13.4%<br>19.9%<br>glm-4.5<br>8.6%<br>23.0%<br>11.3%<br>5.6%<br>16.0%<br>0.0%<br>27.3%<br>16.8%<br>16.6%<br>gpt-5-mini<br>3.4%<br>21.3%<br>9.5%<br>6.2%<br>24.3%<br>0.0%<br>22.6%<br>19.0%<br>16.5%<br>grok-code<br>10.3%<br>22.9%<br>10.6%<br>3.1%<br>17.9%<br>1.6%<br>25.0%<br>13.8%<br>15.5%<br>gemini-2.5-flash<br>10.3%<br>16.3%<br>7.7%<br>1.2%<br>12.8%<br>0.0%<br>16.2%<br>5.2%<br>9.8%<br>deepseek-chat-v3.1<br>3.4%<br>6.9%<br>5.0%<br>1.8%<br>10.2%<br>0.0%<br>8.7%<br>6.5%<br>6.1%<br>model union<br>37.9%<br>55.8%<br>34.8%<br>26.1%<br>46.8%<br>4.8%<br>77.9%<br>38.8%<br>44.3%<br>Lean<br>59 tasks<br>603 tasks<br>440 tasks<br>161 tasks^1<br>189 tasks<br>62 tasks<br>172 tasks<br>675 tasks<br>2361 tasks<br>gpt-5<br>45.8%<br>5.1%<br>32.0%<br>3.7%<br>14.3%<br>12.9%<br>34.9%<br>18.4%<br>17.9%<br>claude-sonnet-4<br>30.5%<br>0.7%<br>11.4%<br>1.2%<br>13.8%<br>1.6%<br>10.5%<br>24.0%<br>11.9%<br>gemini-2.5-pro<br>23.7%<br>0.3%<br>14.1%<br>3.1%<br>12.2%<br>1.6%<br>9.3%<br>19.9%<br>10.9%<br>claude-opus-4.1<br>20.3%<br>1.0%<br>11.8%<br>3.1%<br>15.3%<br>1.6%<br>10.5%<br>19.3%<br>10.7%<br>gpt-5-mini<br>15.3%<br>0.3%<br>15.0%<br>0.0%<br>1.6%<br>1.6%<br>4.1%<br>6.8%<br>5.7%<br>grok-code<br>10.2%<br>0.0%<br>9.1%<br>0.0%<br>1.1%<br>0.0%<br>4.7%<br>6.2%<br>4.2%<br>glm-4.5<br>6.8%<br>0.2%<br>2.5%<br>0.0%<br>0.5%<br>0.0%<br>1.7%<br>2.7%<br>1.6%<br>gemini-2.5-flash<br>0.0%<br>0.2%<br>0.5%<br>0.0%<br>0.0%<br>0.0%<br>0.6%<br>1.9%<br>0.7%<br>deepseek-chat-v3.1<br>0.0%<br>0.0%<br>0.0%<br>0.0%<br>0.0%<br>0.0%<br>0.0%<br>0.1%<br>0.0%<br>model union<br>52.5%<br>7.6%<br>34.1%<br>8.1%<br>25.4%<br>12.9%<br>44.2%<br>38.5%<br>26.8%<br>1<br>From the CLEVER benchmark |
| --- |
| Additional results<br>gpt-5<br>gemini-pro<br>gpt-mini<br>opus<br>grok-c<br>sonnet<br>glm<br>deepseek<br>gemini-fl<br>union<br>(A) 4006 tasks<br>38.0%<br>12.7%<br>6.2%<br>6.1%<br>4.5%<br>4.0%<br>1.7%<br>0.1%<br>0.1%<br>41.8%<br>(B) 782 tasks<br>72.0%<br>75.3%<br>89.2%<br>82.1%<br>85.2%<br>81.6%<br>73.8%<br>96.8%<br>(768)<br>(437)<br>(782)<br>(782)<br>(782)<br>(278)<br>(621)<br>(C) 157 tasks<br>Dafny +vibe<br>76.4%<br>66.8%<br>73.9%<br>73.2%<br>63.0%<br>72.0%<br>50.9%<br>46.4%<br>45.9%<br>87.3%<br>Dafny +vibe<br>68.8%<br>68.8%<br>72.0%<br>66.9%<br>58.6%<br>70.1%<br>51.6%<br>42.7%<br>49.0%<br>86.6%<br>Verus +vibe<br>30.7%<br>25.6%<br>24.3%<br>26.2%<br>17.9%<br>27.5%<br>16.0%<br>10.2%<br>12.8%<br>46.8%<br>Verus +vibe<br>22.4%<br>25.6%<br>17.9%<br>22.4%<br>18.5%<br>23.7%<br>12.8%<br>10.2%<br>18.5%<br>37.8%<br>(A) FVAPPS in Lean  (B) DafnyBench verification  (C) Spec+vibe vericoding for Verina |

## 5 Conclusions

We have made the case for vericoding as a rigorous alternative to vibe coding, released by far the largest vericoding benchmark to date, and demonstrated success rates ranging from 27% for Lean to 82% for Dafny. The rapid rate of LLM progress (improving formal verification success from 68% to 96% in just over a year) appears likely to futher improve vericoding success in the near future.
As AI-generated code becomes more widely deployed, formal verification will become increasingly critical for ensuring code correctness.

Our contributions complement concurrent efforts such as cslib (Montesi et al., 2025), which provides additional Lean tasks that we can now approach with LLM-generated solutions.

We see many opportunities for improving our results. While the tasks in our dataset are typically solvable in under 100 lines of code, extending formal specs to more complex benchmarks like SWE-bench (Jimenez et al., 2024) or BashBench (Bhatt et al., 2025) presents exciting future challenges.
Our current results, achieved without extensive prompt optimization, also suggest significant room for improvement through more advanced techniques such as tree search and reinforcement learning approaches, e.g., see Seed-Prover (Chen et al., 2025).
Future work could also explore networks of collaborative LLMs, each leveraging their unique strengths to tackle verification problems.

Acknowledgements: The authors wish to thank Hantao Luo for submitting helpful Lean NumPy specifications to the benchmark.

## References

- Aggarwal et al. (2024)
Pranjal Aggarwal, Bryan Parno, and Sean Welleck.
AlphaVerus: Bootstrapping formally verified code generation through
self-improving translation and treefinement.
*CoRR*, abs/2412.06176, 2024.
doi: 10.48550/ARXIV.2412.06176.
URL [https://doi.org/10.48550/arXiv.2412.06176](https://doi.org/10.48550/arXiv.2412.06176).
- Alur et al. (2018)
Rajeev Alur, Rishabh Singh, Dana Fisman, and Armando Solar-Lezama.
Search-based program synthesis.
*Communications of the ACM*, 61(12):84–93,
2018.
- (3)
Archive of Formal Proofs.
The archive of formal proofs, 2025.
URL [https://www.isa-afp.org/](https://www.isa-afp.org/).
- (4)
Ariane 5 Failure.
Ariane 5 failure, 1996.
URL
[https://www.esa.int/Newsroom/Press_Releases/Ariane_501_-_Presentation_of_Inquiry_Board_report](https://www.esa.int/Newsroom/Press_Releases/Ariane_501_-_Presentation_of_Inquiry_Board_report).
- Barbosa et al. (2021)
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers,
Kevin Liao, and Bryan Parno.
Sok: Computer-aided cryptography.
In *42nd IEEE Symposium on Security and Privacy, SP 2021,
San Francisco, CA, USA, 24-27 May 2021*, pp. 777–795. IEEE, 2021.
doi: 10.1109/SP40001.2021.00008.
URL [https://doi.org/10.1109/SP40001.2021.00008](https://doi.org/10.1109/SP40001.2021.00008).
- Beyer & Strejček (2025)
Dirk Beyer and Jan Strejček.
Improvements in software verification and witness validation: Sv-comp
2025.
In Arie Gurfinkel and Marijn Heule (eds.), *Tools and Algorithms
for the Construction and Analysis of Systems*, pp. 151–186, Cham, 2025.
Springer Nature Switzerland.
ISBN 978-3-031-90660-2.
- Bhatt et al. (2025)
Aryan Bhatt, Cody Rushing, Adam Kaufman, Tyler Tracy, Vasil Georgiev, David
Matolcsi, Akbir Khan, and Buck Shlegeris.
Ctrl-Z: Controlling AI agents via resampling, 2025.
URL [https://arxiv.org/abs/2504.10374](https://arxiv.org/abs/2504.10374).
- Chen et al. (2025)
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan
Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen,
Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui
Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang,
Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang,
Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu.
Seed-prover: Deep and broad reasoning for automated theorem proving,
2025.
URL [https://arxiv.org/abs/2507.23726](https://arxiv.org/abs/2507.23726).
- Chen et al. (2021)
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé
de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph,
Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy
Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder,
Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens
Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias
Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss,
William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor
Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher
Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Misra, Evan Morikawa,
Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter
Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and
Wojciech Zaremba.
Evaluating large language models trained on code.
*CoRR*, abs/2107.03374, 2021.
URL [https://arxiv.org/abs/2107.03374](https://arxiv.org/abs/2107.03374).
- (10)
CrowdStrike Outage.
Crowdstrike outage, 2024.
URL
[https://www.nytimes.com/2024/07/19/business/dealbook/tech-outage-crowdstrike-microsoft.html](https://www.nytimes.com/2024/07/19/business/dealbook/tech-outage-crowdstrike-microsoft.html).
- Deng et al. (2025)
Xun Deng, Sicheng Zhong, Andreas Veneris, Fan Long, and Xujie Si.
Verifythisbench: Generating code, specifications, and proofs all at
once, 2025.
URL [https://arxiv.org/abs/2505.19271](https://arxiv.org/abs/2505.19271).
- Dougherty & Mehta (2025)
Quinn Dougherty and Ronak Mehta.
Proving the coding interview: A benchmark for formally verified code
generation, 2025.
URL [https://arxiv.org/abs/2502.05714](https://arxiv.org/abs/2502.05714).
- Elsworth et al. (2025)
Cooper Elsworth, Keguo Huang, David Patterson, Ian Schneider, Robert Sedivy,
Savannah Goodman, Ben Townsend, Parthasarathy Ranganathan, Jeff Dean, Amin
Vahdat, Ben Gomes, and James Manyika.
Measuring the environmental impact of delivering ai at google scale,
2025.
URL [https://arxiv.org/abs/2508.15734](https://arxiv.org/abs/2508.15734).
- (14)
Google Earnings Call.
Google earnings call q1 2025, 2025.
URL [https://abc.xyz/2025-q1-earnings-call/](https://abc.xyz/2025-q1-earnings-call/).
- Greenblatt et al. (2024)
Ryan Greenblatt, Buck Shlegeris, Kshitij Sachan, and Fabien Roger.
AI control: Improving safety despite intentional subversion, 2024.
URL [https://arxiv.org/abs/2312.06942](https://arxiv.org/abs/2312.06942).
- Harmonic (2025)
Harmonic.
Running lean at scale, September 2025.
URL [https://harmonic.fun/news#blog-post-lean](https://harmonic.fun/news#blog-post-lean).
Blog post.
- Harris et al. (2020)
Charles R. Harris, K. Jarrod Millman, Stéfan J. van der Walt, Ralf
Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor,
Sebastian Berg, Nathaniel J. Smith, Robert Kern, Matti Picus, Stephan Hoyer,
Marten H. van Kerkwijk, Matthew Brett, Allan Haldane, Jaime Fernández
del Río, Mark Wiebe, Pearu Peterson, Pierre Gérard-Marchant,
Kevin Sheppard, Tyler Reddy, Warren Weckesser, Hameer Abbasi, Christoph
Gohlke, and Travis E. Oliphant.
Array programming with NumPy.
*Nature*, 585(7825):357–362, September
2020.
doi: 10.1038/s41586-020-2649-2.
URL [https://doi.org/10.1038/s41586-020-2649-2](https://doi.org/10.1038/s41586-020-2649-2).
- Hendrycks et al. (2021)
Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora,
Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, and Jacob
Steinhardt.
Measuring coding challenge competence with apps, 2021.
URL [https://arxiv.org/abs/2105.09938](https://arxiv.org/abs/2105.09938).
- JetBrains-Research (2025)
JetBrains-Research.
Verified code benches, 2025.
URL
[https://github.com/JetBrains-Research/verified-cogen/tree/main/benches](https://github.com/JetBrains-Research/verified-cogen/tree/main/benches).
- Jiang et al. (2024)
Albert Q. Jiang, Alexandre Sablayrolles, Antoine Roux, Arthur Mensch, Blanche
Savary, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Emma Bou
Hanna, Florian Bressand, Gianna Lengyel, Guillaume Bour, Guillaume Lample,
Lélio Renard Lavaud, Lucile Saulnier, Marie-Anne Lachaux, Pierre Stock,
Sandeep Subramanian, Sophia Yang, Szymon Antoniak, Teven Le Scao, Théophile
Gervet, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed.
Mixtral of experts, 2024.
URL [https://arxiv.org/abs/2401.04088](https://arxiv.org/abs/2401.04088).
- Jiang et al. (2021)
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu.
Lisa: Language models of isabelle proofs.
In *6th Conference on Artificial Intelligence and Theorem
Proving*, pp. 378–392, 2021.
- Jimenez et al. (2024)
Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir
Press, and Karthik Narasimhan.
Swe-bench: Can language models resolve real-world github issues?,
2024.
URL [https://arxiv.org/abs/2310.06770](https://arxiv.org/abs/2310.06770).
- Johnson et al. (2017)
Jeff Johnson, Matthijs Douze, and Hervé Jégou.
Billion-scale similarity search with gpus, 2017.
URL [https://arxiv.org/abs/1702.08734](https://arxiv.org/abs/1702.08734).
- Lample et al. (2022)
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury
Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix.
Hypertree proof search for neural theorem proving, 2022.
URL [https://arxiv.org/abs/2205.11491](https://arxiv.org/abs/2205.11491).
- Lattuada et al. (2024)
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley
LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon
Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno.
Verus: A practical foundation for systems verification.
In Emmett Witchel, Christopher J. Rossbach, Andrea C.
Arpaci-Dusseau, and Kimberly Keeton (eds.), *Proceedings of the ACM
SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin,
TX, USA, November 4-6, 2024*, pp. 438–454. ACM, 2024.
doi: 10.1145/3694715.3695952.
URL [https://doi.org/10.1145/3694715.3695952](https://doi.org/10.1145/3694715.3695952).
- Leino (2010)
K. Rustan M. Leino.
Dafny: An automatic program verifier for functional correctness.
In Edmund M. Clarke and Andrei Voronkov (eds.), *Logic for
Programming, Artificial Intelligence, and Reasoning - 16th International
Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected
Papers*, volume 6355 of *Lecture Notes in Computer Science*, pp. 348–370. Springer, 2010.
doi: 10.1007/978-3-642-17511-4“˙20.
URL [https://doi.org/10.1007/978-3-642-17511-4_20](https://doi.org/10.1007/978-3-642-17511-4_20).
- Li et al. (2022)
Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser,
Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago,
et al.
Competition-level code generation with alphacode.
*Science*, 378(6624):1092–1097, 2022.
- Lin et al. (2024)
Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying
Liu, Linqi Song, and Xiaodan Liang.
Fvel: Interactive formal verification environment with large language
models via theorem proving, 2024.
URL [https://arxiv.org/abs/2406.14408](https://arxiv.org/abs/2406.14408).
- Loughridge et al. (2025)
Chloe R Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun,
Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark.
DafnyBench: A benchmark for formal software verification.
*Transactions on Machine Learning Research*, 2025.
ISSN 2835-8856.
URL [https://openreview.net/forum?id=yBgTVWccIx](https://openreview.net/forum?id=yBgTVWccIx).
- Miranda et al. (2025)
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.
- Montesi et al. (2025)
Fabrizio Montesi, Chris Henson, Kim Morrison, Kenny Lau, euprunin, Tristan
F.-R., Juan Pablo Yamamoto, Maximiliano Onofre-Martínez, Alexandre
Rademaker, Clark Barrett, Xueying Qin, thomaskwaring, thelissimus, and Tanner
Duve.
cslib: The lean library for computer science, 2025.
URL [https://github.com/leanprover/cslib](https://github.com/leanprover/cslib).
GitHub repository.
- Moura & Ullrich (2021)
Leonardo de Moura and Sebastian Ullrich.
The lean 4 theorem prover and programming language.
In *International Conference on Automated Deduction*, pp. 625–635. Springer, 2021.
- Peng et al. (2024)
Qiwei Peng, Yekun Chai, and Xuhong Li.
Humaneval-xl: A multilingual code generation benchmark for
cross-lingual natural language generalization.
*arXiv preprint arXiv:2402.16694*, 2024.
- Polu & Sutskever (2020)
Stanislas Polu and Ilya Sutskever.
Generative language modeling for automated theorem proving, 2020.
URL [https://arxiv.org/abs/2009.03393](https://arxiv.org/abs/2009.03393).
- Polubelova (2022)
Marina Polubelova.
*Building a Formally Verified High-Performance Multi-Platform
Cryptographic Library in F*. (Construction d’une bibliothèque
cryptographique multi-plateformes formellement vérifiée à
haute performance en F*)*.
PhD thesis, Université Paris sciences et lettres, Paris, France,
2022.
URL [https://tel.archives-ouvertes.fr/tel-03981965](https://tel.archives-ouvertes.fr/tel-03981965).
- Reimers & Gurevych (2019)
Nils Reimers and Iryna Gurevych.
Sentence-bert: Sentence embeddings using siamese bert-networks.
In *Proceedings of the 2019 Conference on Empirical Methods in
Natural Language Processing and the 9th International Joint Conference on
Natural Language Processing (EMNLP-IJCNLP)*, pp. 3982–3992, Hong Kong,
China, November 2019. Association for Computational Linguistics.
doi: 10.18653/v1/D19-1410.
URL [https://arxiv.org/abs/1908.10084](https://arxiv.org/abs/1908.10084).
- (37)
Shellshock Bug.
Shellshock bug, 2014.
URL
[https://www.enisa.europa.eu/publications/info-notes/flash-note-the-bash-shellshock-bug](https://www.enisa.europa.eu/publications/info-notes/flash-note-the-bash-shellshock-bug).
- Thakur et al. (2025)
Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao,
Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri.
CLEVER: A curated benchmark for formally verified code
generation.
*CoRR*, abs/2505.13938, 2025.
doi: 10.48550/ARXIV.2505.13938.
URL [https://doi.org/10.48550/arXiv.2505.13938](https://doi.org/10.48550/arXiv.2505.13938).
- Tsoukalas et al. (2024)
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael
Jennings, Amitayush Thakur, and Swarat Chaudhuri.
Putnambench: Evaluating neural theorem-provers on the putnam
mathematical competition, 2024.
URL [https://arxiv.org/abs/2407.11214](https://arxiv.org/abs/2407.11214).
- Turing (1950)
A. M. Turing.
Computing machinery and intelligence.
*Mind*, 59(236):433–460, 1950.
ISSN 00264423.
URL [http://www.jstor.org/stable/2251299](http://www.jstor.org/stable/2251299).
- Yang et al. (2025)
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun
Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang,
Ziqiao Zhou, and Shan Lu.
AutoVerus: Automated proof generation for rust code, 2025.
URL [https://arxiv.org/abs/2409.13082](https://arxiv.org/abs/2409.13082).
- Yang et al. (2023)
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu,
Saad Godil, Ryan Prenger, and Anima Anandkumar.
Leandojo: Theorem proving with retrieval-augmented language models,
2023.
URL [https://arxiv.org/abs/2306.15626](https://arxiv.org/abs/2306.15626).
- Ye et al. (2025)
Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song.
VERINA: benchmarking verifiable code generation.
*CoRR*, abs/2505.23135, 2025.
doi: 10.48550/ARXIV.2505.23135.
URL [https://doi.org/10.48550/arXiv.2505.23135](https://doi.org/10.48550/arXiv.2505.23135).
- Yu et al. (2025)
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu,
Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang,
and Weiyang Liu.
Formalmath: Benchmarking formal mathematical reasoning of large
language models, 2025.
URL [https://arxiv.org/abs/2505.02735](https://arxiv.org/abs/2505.02735).

## Appendix A Appendix

Our Dafny, Lean, Verus benchmarks can be found in our Supplementary Material. In particular, the file benchmarks/vericoding_benchmark_v1.csv contains a summary of the metadata for all 12,504 tasks. The file experiments/vericoding_results_v1.csv contains the outcomes of all 55,397 vericoding experiments, one for each task and each language model.

### 1.1 Original sources

*DafnyBench.* In this source, besides removing existing code and proofs to create a vericoding task, we split the larger files (which contain multiple methods, code and lemmas) into smaller tasks, each with one method and its dependencies. We also filter out files that do not contain any methods.

*Verified Cogen*.This benchmark from JetBrains Research contains Rust programs with Verus specifications focusing on memory safety and functional correctness. To create tasks, we removed implementation bodies.

*Verina and Clever.* The former gathers problems on data structures, algorithms, and mathematical properties, while the latter focuses on functional correctness of algorithms and data structures. We removed all spec generation and spec isomorphism requirements from the tasks.

*APPS and HumanEval.* These are popular coding benchmarks containing Python problems with natural language specifications and test cases. 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. We generated Dafny specifications by means of a specific LLM translator (see Section [3.3](https://arxiv.org/html/2509.22908v1#S3.SS3)).

*FVAPPS.* It translates the *Train* split of the APPS Python benchmark to Lean and adds formal specs. We keep the unit tests for each task and apply them in our vericoding experiments.

*NumPy simple and NumPy triple.*
(Harris et al., 2020). Scraped from numpy docs, checked by hand (we need to recheck considering some specs have slipped past), simple format and triple format. Represent specs as Hoare triples, with preconditions, the program and the postcondition, using new *mvcgen* feature in Lean.

*BigNum.* This is a collection of arithmetic algorithms on big numbers in Dafny that we wrote from scratch: simplified versions of 13 functions often used in cryptography which is a prime target for formal verification (Barbosa et al., 2021). By varying the combination of helper functions included, we obtain 62 tasks.

### 1.2 Licenses

Our code/datasets are released under the MIT License.
Table [4](https://arxiv.org/html/2509.22908v1#A1.T4) shows dataset sources and licenses.

**Table 4: Licenses of dataset sources used in our benchmark**
| Dataset | Source License | Source URL |
| --- | --- | --- |
| APPS (test) | MIT | github.com/hendrycks/apps |
| DafnyBench | Apache 2.0 | github.com/sun-wendy/DafnyBench |
| NumPy Triple | BSD-3-Clause | github.com/numpy/numpy |
| verified-cogen | Permission requested | github.com/JetBrains-Research/verified-cogen |
| Verina | Apache 2.0 | github.com/sunblaze-ucb/verina |
| Bignum | MIT | Our own work |
| NumPy Simple | BSD-3-Clause | github.com/numpy/numpy |
| HumanEval Python | MIT | github.com/openai/human-eval |
| FVAPPS | MIT | huggingface.co/datasets/quinn-dougherty/fvapps |
| Clever | MIT | github.com/trishullab/clever |

### 1.3 Prompts and hyperparameters

The following prompts are used for code generation and verification repair in different languages.

Each LLM had five attempts at a sample: One initial attempt, and four retries with the error message from applying the proof checker to the previous attempt. We did not run multiple trials with a fresh history, but it may be worth looking into whether an LLM gets locked into a bad approach.
For the bignums dataset, we instead gave the LLM one initial attempt and nine retries.

Dafny code generation prompt:

Dafny verification repair prompt:

Verus code generation prompt:

Verus verification repair prompt:

Lean code generation prompt:

Lean verification repair prompt:

### 1.4 Quality Analysis of Specifications

See Table [5](https://arxiv.org/html/2509.22908v1#A1.T5). The table shows the following metrics: “Quality Score” represents a normalized quality metric on a 0-100 scale (higher is better); “Defaults” indicates files with placeholder values; “Sorry Defs” refers to Lean definitions using sorry in vc-preamble; “Ghost Types” denotes Verus files with ghost type issues; and “Duplicates” shows the percentage of near-duplicate entries. The high near-duplicates for Bignum Dafny is by design: we split a few big tasks into many smaller ones.

**Table 5: Detailed Benchmark Quality Metrics**
| Language | Benchmark | Entries | Quality | Defaults | Sorry | Ghost | Duplicates |
| --- | --- | --- | --- | --- | --- | --- | --- |
|  |  |  | Score |  | Defs | Types | (%) |
| Dafny | Apps | 677 | 97.7 | 36 | — | — | 0.9 |
| Dafny | NumPy Triple | 603 | 96.5 | 5 | — | — | 21.2 |
| Dafny | HumanEval | 162 | 96.3 | 7 | — | — | 13.0 |
| Dafny | Metadata | 169 | 96.3 | 7 | — | — | 12.4 |
| Dafny | NumPy Simple | 58 | 96.1 | — | — | — | 25.9 |
| Dafny | DafnyBench | 443 | 93.4 | 3 | — | — | 42.2 |
| Dafny | Verina | 157 | 92.9 | — | — | — | 22.3 |
| Dafny | Verified CoGen | 172 | 92.4 | — | — | — | 50.6 |
| Dafny | BigNum | 62 | 85.2 | — | — | — | 98.4 |
| Lean | Apps | 676 | 99.6 | — | 3 | — | 0.0 |
| Lean | FV Apps | 4,006 | 99.3 | — | — | — | 4.5 |
| Lean | CLEVER | 161 | 97.6 | — | — | — | 16.1 |
| Lean | Verified CoGen | 172 | 96.4 | — | — | — | 23.8 |
| Lean | Verina | 189 | 96.1 | — | — | — | 25.9 |
| Lean | NumPy Simple | 59 | 93.9 | — | — | — | 40.7 |
| Lean | DafnyBench | 440 | 92.9 | — | 1 | — | 46.1 |
| Lean | NumPy Triple | 603 | 92.4 | — | — | — | 50.9 |
| Lean | BigNum | 62 | 18.3 | — | 49 | — | 96.8 |
| Verus | Apps | 536 | 99.4 | 4 | — | — | 2.6 |
| Verus | NumPy Triple | 581 | 97.2 | 1 | — | 5 | 16.5 |
| Verus | HumanEval | 161 | 95.9 | 10 | — | 4 | 10.6 |
| Verus | NumPy Simple | 58 | 95.3 | — | — | — | 31.0 |
| Verus | Verina | 156 | 94.0 | — | — | 18 | 20.5 |
| Verus | Verified CoGen | 172 | 91.1 | — | — | — | 59.3 |
| Verus | DafnyBench | 440 | 85.6 | 1 | — | 150 | 38.6 |
| Verus | BigNum | 62 | 85.5 | — | — | — | 96.8 |

#### 1.4 .1 Near-duplicates

See Figure [5](https://arxiv.org/html/2509.22908v1#A1.F5).

Figure: Figure 5: Near-duplicate Dafny files

### 1.5 Vericoding Examples

To complement Figure [1](https://arxiv.org/html/2509.22908v1#S3.F1), Figure [6](https://arxiv.org/html/2509.22908v1#A1.F6) shows examples of vericoding tasks in different languages and of vibe coding.

Figure: Figure 6:

#### 1.5 .1 Problematic Specifications

Figure [7](https://arxiv.org/html/2509.22908v1#A1.F7) shows examples of default values from specifications: (a) from an underspecified source spec, and (b) from an incomplete source spec.

Figure: (a) The Lean spec provides less information, thus the verus translation is weak as well.

#### 1.5 .2 Incomplete code

Figure [8](https://arxiv.org/html/2509.22908v1#A1.F8) shows an example where the LLM exploits an incomplete spec.
This is LC0033, which was obtained from the CLEVER benchmark (Thakur et al., 2025).

Figure: (a) The spec is meant to sort and deduplicate a list

#### 1.5 .3 Successful vericoding

Figure [9](https://arxiv.org/html/2509.22908v1#A1.F9) shows an example where GPT-5 successfully implemented a Fibonacci recursion in Lean. This is LC0045, obtained from the CLEVER benchmark (Thakur et al., 2025).

Figure: (a) A Fibonacci spec

### 1.6 DafnyBench verification

To test LLM performance on the original dataset (Loughridge et al., 2025), we use the original prompts and evaluation metrics over $n=10$ attempts. We increase the max token limit from 4096 to 8196 with a timeout of 120 seconds due to longer chain of thought in recent models. If we reach the max token limit, we retry the current attempt $n=3$ times, reporting a failed attempt if there is no successful retry. This explains the lower GPT-5 accuracy but higher model union accuracy. With some models, we weren’t able to sample the full 782 problems, so we sampled a random subset as a representative sample. The number of samples is given in Table [3](https://arxiv.org/html/2509.22908v1#S4.T3).

### 1.7 Ethics Statement

We acknowledge that running LLMs creates carbon emissions, e.g. 0.24 Wh per request for Gemini (Elsworth et al., 2025).
We believe the value of reducing bugs outweighs carbon emissions.

### 1.8 Reproducibility Statement

The supplementary material includes scripts that can replicate our results. 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. We spent about $25,000 on Open Router. It is not necessary to spend this much to replicate our results. For instance, we found that GPT-5 did better than Gemini 2.5 Pro on the 4006 tasks of FVAPPS (38.0% vs 12.7%). This difference is large enough that running on a random sample of 100 tasks will replicate that result.

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

### 1.9 LLM Usage in Paper Preparation

We used LLMs for the following purposes during the preparation of this paper:

- •
For retrieval and discovery, such as looking up related works on verification benchmarks;
- •
To write scripts for translating, formatting, quality-checking, experiments and analysis;
- •
To aid or polish writing, such as fixing grammatical mistakes.
- •
To help debug LaTeX

## Peer Reviews

confidence: 4
contribution: 2
initial_rating: 2
presentation: 3
questions: Please address my comments in the “Weakness” section.
soundness: 1
strengths: 1. Introduces a large-scale dataset on a timely and impactful topic—AI-assisted formal verification.
2. Covers diverse verification frameworks (Dafny, Verus, Lean), enabling cross-system comparisons between ATP and ITP paradigms.
3. Provides comprehensive LLM evaluations, revealing quantitative differences across languages and models.
4. Transparent methodology with anti-cheating validation and manual inspection reports.
5. Clear writing.
summary: This paper introduces a comprehensive and large benchmark for the automatic generation of formally verified programs given formal specifications. The benchmark spans three verification frameworks (Dafny, Verus, and Lean), covering both automated theorem provers (ATPs) and interactive theorem provers (ITPs). It aggregates and translates tasks from multiple prior sources (e.g., DafnyBench, Verina, FVAPPS, HumanEval) into a unified suite of 12,504 tasks, of which 6,174 are new. The authors evaluate a broad range of LLMs (GPT-5, Claude, Gemini, etc.) on this benchmark, achieving best results in Dafny (82.2% success) and lower rates for Verus (44.3%) and Lean (26.8%). The study aims to provide a foundation for measuring LLM progress in generating provably correct code.
weaknesses: 1. Conceptual limitation of the “vericoding” definition: The paper defines vericoding narrowly as code and proof generation from formal specifications, explicitly excluding specification generation. However, specification writing is the main bottleneck in formal verification and a key component of prior benchmarks such as CLEVER and VERINA. By ignoring spec generation, this benchmark captures only a partial and arguably easier slice of the full verified-coding problem. This weakens the practical and conceptual impact of the work.

2. I find the benchmark quality to be weak, for reasons detailed below. This is a major limitation, especially because the work targets formal verification—a domain that demands the highest level of rigor. If the benchmark itself includes incomplete or incorrect specifications, it cannot faithfully measure models’ verification capabilities and may even lead to misleading or unsafe outcomes if such models are later used in production settings.
    - The spec translation and validation rely on an LLM judge to assess semantic equivalence, which may not guarantee correctness. The verifier only ensures syntactic validity.
    - I appreciate the authors’ manual inspection and being upfront about weak specification or other problems with the benchmark. However, the description reads vague to me: “Verus showed *many* weak specs due to spec translation issues, e.g. deviations from the original BigNum specs in Dafny. Lean displayed *occasional* redundant lemma additions during vericoding, and had *some* weak specs from the original sources.”. Could you provide quantitative measures? 
    - The authors also did not seem to talk about how specifications identified as low quality are processed. Are they still included in the benchmark, or are they fixed? My impression is that they are still included.
    - The current quality score of the benchmark is a weighted average of several defined criterias, which only consider obvious cases (including defaults, sorry defs, ghost types, duplication), but do not measure the semantic quality of the specification.

3. The evaluation settings are unclear and lack important baselines.
    - The paper does not specify how many refinement iterations are allowed, what error messages are fed back, or whether these differ across verification frameworks. Moreover, how do these choices impact performance?
    - Only general-purpose LLMs are tested. No experiments with proof-specialized approaches (e.g., DeepSeek-Prover-V2 [1], Goedel-Prover-V2 [2], SAFE [3], AutoVerus [4], AlphaVerus [5]) are included.

4. Overall, the benchmark emphasizes scale, but size alone does not determine effectiveness. Beyond quality, a benchmark should be diverse enough to cover a broad spectrum of difficulty levels to meaningfully differentiate model capabilities. In fact, without such diversity, a large benchmark can even become a costly burden for evaluation, obscuring rather than clarifying model progress. In this regard, I think the paper is doing a good job in including both ATPs and ITPS. However, In Table 2, although multiple benchmark sources are combined, the paper does not discuss the degree of overlap among these sources or the relative difficulty of the tasks they contribute. It is therefore unclear whether the enlarged dataset truly expands task diversity or merely aggregates similar problems, which raises questions about how well the benchmark can measure real advances in verification performance. For example, in Table 3, the performance trend on the Verina subset closely mirrors the overall average, suggesting limited incremental value. If that is the case, why not evaluate directly on the Verina subset instead?

[1] Ren, Z. Z., et al. "Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition." arXiv preprint arXiv:2504.21801 (2025).

[2] Lin, Yong, et al. "Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction." arXiv preprint arXiv:2508.03613 (2025).

[3] Chen, Tianyu, et al. "Automated proof generation for rust code via self-evolution." ICLR 2025.

[4] Yang, Chenyuan, et al. "Autoverus: Automated proof generation for rust code." Proceedings of the ACM on Programming Languages 9.OOPSLA2 (2025): 3454-3482.

[5] Aggarwal, Pranjal, Bryan Parno, and Sean Welleck. "Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement." ICML 2025.

---

confidence: 4
contribution: 2
initial_rating: 4
presentation: 2
questions: - Is there a plan to release a cleaned version of the benchmark that addresses the 24% of problematic specifications?
- How is the inclusion of 98.4% near-duplicate tasks justified, and shouldn't these be deduplicated?
- Is every task in the benchmark provable, meaning each has a ground-truth code and proof?
- Can the manual inspection process be expanded beyond the current 5 samples, which represent less than 1% coverage?
soundness: 2
strengths: - Unprecedented Scale: With 12,504 tasks, this benchmark is two orders of magnitude larger than existing verification benchmarks, addressing a significant gap in the field.
- Comprehensive Language Coverage: It includes both Automated Theorem Provers (ATPs) like Dafny and Verus, and Interactive Theorem Provers (ITPs) such as Lean, thereby enabling cross-paradigm comparisons.
summary: This paper introduces a substantial vericoding benchmark, encompassing 12,504 formal specifications. These specifications are divided among Dafny (3,029), Verus (2,334), and Lean (7,141), with 6,174 being newly developed problems. Vericoding distinguishes itself from end-to-end generation by requiring Large Language Models (LLMs) to generate both implementations and their corresponding proofs from existing formal specifications, rather than inferring the specifications themselves. Current frontier LLMs demonstrate varying success rates: 82% for Dafny, 44% for Verus, and 27% for Lean.
weaknesses: - Duplication Concerns: Figure 5 highlights the presence of near-duplicate tasks, which are essentially the same problem with minor variations. This issue artificially inflates the benchmark's size and reduces its overall diversity.
- Limited Quality Validation: The study only examines 5 tasks per model and source, indicating a lack of systematic evaluation regarding the quality of the benchmark tasks.
- Insufficient Evaluation and Analysis: Figure 4's analysis is restricted to length metrics, which are obvious predictors. The paper lacks investigation into crucial aspects such as: factors contributing to task difficulty (e.g., proof complexity, theorem depth), reasons behind different models' varying performance across languages.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: Could you discuss the challenge of translating specifications between theorem provers in a formal manner?
soundness: 3
strengths: - A comprehensive vericoding benchmark set is good to have, given that there has been significant research interest in this area.
- The paper uses iterative refinement coupled with verification to improve the success rate of the translation.
- The paper identifies several additional potential issues that may hamper the quality of the benchmark, and describes ways to mitigate them.
- The experimental evaluation is quite thorough and gives a nice overview of the current landscape of LLM capability in vericoding.
summary: This paper introduces a benchmark set for vericoding, which is the task of synthesizing formally verified code (including proofs) from formal specifications. The benchmark set contains benchmarks for Dafny, Verus, and Lean. The benchmarks are generated from multiple sources:
1. cross translation into target languages from existing verification benchmarks; 
2. auto-formalizing vibe-coding benchmarks;
3. auto-formalizing documentation of libraries such as NumPy and BigNum.

The paper describes several ways employed to ensure the quality of the benchmarks. The paper also includes a thorough evaluation of a range of LLMs on this benchmark.
weaknesses: - The language-to-language generation process is LLM-based, which is a little sloppy and itself error-prone. I understand that translating proofs between theorem provers can be challenging (and, anyway, verification can ensure the soundness of the proof), but I wonder whether translating the specifications can be done in a more rigorous manner, using analytical approaches. 
- Although the paper seems to have spent non-trivial effort to ensure the quality of the benchmarks, the quality of the benchmarks is still not close to being perfect (9% weak specs and 15% incorrect translation).

---

confidence: 4
contribution: 1
initial_rating: 2
presentation: 2
questions: * Why is FVAPPS categorized as a "vibe coding" benchmark instead of vericoding?
soundness: 3
strengths: I agree with the high-level motivation of this work. Generating formally verifiable code is important and will be more important in the near future as LLMs become better at code generation. Well-constructed benchmarks in this space will unleash research progress.
summary: The paper's main contribution is to introduce a benchmark for "vericoding" (defined in this paper as generating code + proof given a formal spec). Data examples in this benchmark were curated by pulling together existing vericoding benchmarks in different formal languages (Lean, Dafny, Verus) and using LLMs to translate between them, as well as autoformalizing coding benchmarks such as APPS. The authors also evaluated many off-the-shelf LLMs such as GPT-5 on the new benchmark and performed analysis on the results.
weaknesses: However, I'm not convinced by the quality of the proposed benchmark and the method for constructing it. Specifically:

* Most examples in the benchmark were either directly from existing benchmarks in different languages (Dafny, Lean, Verus) or obtained by using LLMs to translate between them. It is not clear what value the new benchmark brings or why would a subsequent work evaluate on this new benchmark instead of on multiple existing benchmarks individually.

* The quality of the benchmark is not clear. Only a subset of the translated problems are manually inspected by humans. Many translated specs may be too weak (Line 370). The authors argue that perfect translation is not required; as long as a spec is syntactically valid, it can potentially be a useful task for training or evaluation. I agree the translation doesn't need to be perfect, but it needs to above a certain level for the benchmark to be useful. 

* The new benchmark's data sources (CLEVER, Verina, HumanEval, etc.). For example, CLEVER translated HumanEval into Lean. It's not clear why the authors attempted to translate HumanEval again. 

* This paper uses "Vibe coding" to refer to the dominant approach to AI code generation that does not involve formal methods. For example, in Line 24, the authors claim that Google is using "vibe coding" to generate over 30% of its software, which sounds astonishing. However, what the cited report actually says is over 30% of the code was generated by AI and accepted by human engineers. The research on AI for code generation has a long history and shouldn't be referred to as "vibe coding" (a term coined by Andrej Karpathy in a tweet in 2025 and is often used in the context of LLM coding agents such as Claude Code) in a serious academic publication.

 * The paper introduced a new term "vericoding" to refer to generating code and proof given a formal spec. This task is usually called verified (or verifiable) code generation in recent papers (CLEVER, FVAPPS, Verina, etc.). Before that, program synthesis from formal specification is a well-established task in the PL community.


Decision: Reject