AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
Authors: Pranjal Aggarwal
Bryan Parno
Sean Welleck
Venue: ICML 2025 poster (2025)
Keywords: formal verification
code generation
self-improvement
inference compute
Primary area: deep_learning->large_language_models
TL;DR: AlphaVerus leverages self-improvement and formal verification to generate provably correct code by using exploration, code refinement via tree search, preventing reward hacking and demonstrating state-of-the-art verified code generation capabilities.

Abstract: Automated code generation with large language models has gained significant traction, but there remains no guarantee of the correctness of generated code. We aim to use formal verification to provide mathematical guarantees that the generated code is correct. However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. To tackle this challenge, we introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation by iteratively translating programs from a higher-resource language and leveraging feedback from a verifier. AlphaVerus operates in three phases: exploration of candidate translations, Treefinement -- a novel tree search algorithm for program refinement using verifier feedback, and filtering misaligned specifications and programs to prevent reward hacking. Through this iterative process, AlphaVerus enables the LLaMA-3.1-70B model to generate verified code without human intervention or model finetuning. AlphaVerus shows an ability to generate formally verified solutions for HumanEval and MBPP, laying the groundwork for truly trustworthy code-generation agents.

AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
Pranjal Aggarwal
Bryan Parno !
Sean Welleck
Abstract
ing from fixing bugs in software repositories to solving Olympiad-level algorithmic problems (Jimenez et al., 2024; Li et al., 2022). Despite these successes, multiple stud- ies have identified disturbing mistakes in LLM-produced code, including subtle bugs and serious security vulnerabili- ties (Hendler, 2023; Pearce al., 2021; Jesse al., 2023; Zhong & Wang, 2024; Perry al., 2023; Elgedawy et al., 2024). Ultimately, these mistakes stem from a fundamental property of LLMs: language models can generate any string of code, without regard to correctness. As result, automat- ically checking the correctness of LLM -LM-geeertted code is one of the grand challenges facing the research community.
Automated code generation with large language models has gained significant traction, but there remains no guarantee of the correctness of gen- erated code. We aim to use formal verification to provide mathematical guarantees that the gen- erated code is correct. However, generating for- mally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. To tackle this challenge, we in- troduce Al AlphaVerus, self-improvin frame- work that bootstraps formally verified code gen- eration by iteratively translating programs from a higher-resource language and leveraging feed- back from a verifier. AlphaVerus operates in three phases: exploration of candidate transla- tions, Treefinement-a novel tree search algo- rithm for program refinement using verifier feed- back, and filtering misaligned specifications and programs to prevent reward hacking. Through this iterative process, A1 phaVerus enables the LLaMA- 3. 3-1BBB model to generate verified code without human intervention or model fine- tuning. Alphauerus shows an ability to gen- erate formally verified solutions for HumanEval and MBPP, laying the groundwork for truly trust- worthy code oode-generation agents.'
The generated code must be correct for all possible inputs it may receive. However, today's code generation methods select or filter generations with imperfect proxies of correct- ness, such as runtime testing or human inspection. Achiev- ing perfect test coverage is typically infeasible (Li et al., 2022; Liu et al., 2023), and incomplete coverage leads to an unreliable signal that can exploited by model (Pan et al., 2022; Liu et al., 2023; Denison et al., 2024). Relying on hu- man review is equally problematic since it scales poorly and humans can struggle to tell whether LLM- LLM- generaatedd code is correct (Perry et al., 2023). In turn, the difficulty of trusting generated code reduces the potential productivity gains from using LLMs and can lead to unexpected vulnerabilities or unreliable signals for improving models.
In contrast, generating code in a verification-awwre program- ming language such as Dafny (Leino, 2010), F* (Swamy et al., 2016), or Verus (Lattuada et al., 2023; 2024) offers promising approach to addressing these challenges by providing mathematical guarantees that a program obeys a specification for all possible inputs. In this paradigm, code is paired with a specification and proof written a specialized language, and a mechanical verifier checks whether the code meets the specification. This could dramatically improve the trustworthiness of the generated code: if the verifier passes, the LLM's generated program is mathematically guaranteed to meet the specification. However, writing formal specifica- tions and proofs introduces additional layers of complexity. Furthermore, although LLMs have demonstrated success in automated theorem proving in mathematical domains (Lu et al., 2023; Li al., 2024), their capability to generate
1. Introduction
There has been an enormous effort to train gode-genera large language models (LLMs) (Chen et al., 2021; Austin et al., 2021; Li al., 2023; Rozière et al., 2024; Team, 2024), leading -.oe-e agents that can perform tasks rang-
'Carnegie Mellon University. Correspondence to: Pranjal Ag- garwal <pranjala @ cmw.edu>, Bryan Parno spamo@cmu.eduu Sean Welleck <wellecks @ @mw..dd..mmm........
Proceedings of the 4nnd International Conference on Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
Coode is available httpa:// / alphaverus thub.

---

AlphaVerus
Exploration
Treefinement
Source (e.g. Dafny)
Translations (Verus)
Invalld
Unverified
Examples
Unverified
Verified
Examples
Program Errors
Refliee
LLM
Verifier
Verified
Self-Improvement
Critique
New Translation Examples
Better Exploration
Comparison
Exploit
New Correction Examples
Better Treefinement
Verified
Rule- Fule-based
Verified
Exploit Examples
Critique
Aligned
Figure 1: Overview of AlphaVerus, a self improviig framework for generating formally verified code. Each iteration
consists of three key steps: (1) Exploration translates programs from source language to Verus by sampling multiple trajectories and selecting partially correct ones using verifier feedback, (2) Treefinement iteratively fixes errors guided by verifier feedback and tree search, and (3) Critique validates and filters out underspecified or incorrect translations. The framework bootstraps new exemplars after each iteration continuously improve performance without human intervention.
verified code for even basic algorithms is limited (Sun et al., 2024a; Lohn & Welleck, 2024).
feedback from the verifier, saving the final verified program, along with its ancestors to serve ples. We show that Treefinement leads to substantial gains over vanilla refinement strategies that resemble those used in concurrent work (Yang et al., 2024; Chen et al., 2024). Third, critique models detect misaligned translations and specifications the one part of the pipeline that lacks formal guarantees. Crucially, this alleviates reward hacking, in which models learn to game the system by generating trivial or incomplete specifications, or even by identifying verifier limitations that cause trivial programs to pass the verifier. While previous work has investigated methods that rely on test cases (Sun et al., 2024a), our critique models address the challenging problems of automated specification generation and validation without relying on any unit test cases.
correction exam-
A sigmificant barrier to automatically generating real-world, formally verified code is the scarcity of training data. In particular, verification-awarr research languages have a rich history (e.g., Dafny (Leino, 2010) or (Swamy et al., 2016)), yet verifying real-world code in mainstream lan- guages remains nascent. For example, Verus (Lattuada et al., 20230 verification language for the very popular language Rust-has fewer than 10 public repositories, de- spite Rust itself having millions of code examples. Hence, enabling formally verified code generation in a mainstream language such as Rust faces bootstrapping problem: with- out training data, how do we create an initial model that can generate even relatively simple verified programs?
Each iteration of AlphaVerus collects new exemplars that improve the models in each phase, creating cycle of improvement. Thus, unlike recent work that relies on hu- man experts to write correction prompts (Yang et al., 2024), our method requires no human intervention and automati- cally learns to generate better code. Moreover, the system operates using single language model (e.g., Llama 70b), without the need for the expensive GPT-4 initialization used in concurrent work (Chen et al., 2024). Finally, the collected exemplars can be used to improve the verified code genera- tion performance of any model without any finetuning.
We propose AlphaVerus, framework for bootstrapping formally verified code generation model by iteratively translating programs from a resource-rich domain and self- improving using feedback from the verifier. As illustrated in Figure 1, each iteration of A AlphaVerus has three phases. First, the exploration phase generates candidate programs by translating from source language (such as Dafny) to the tar- get language (here, Verus) by generating multiple candidates and saving partially and completely verified attempts. Sec- ond, Treefinement refines the imperfect candidates through a novel tree search over the space of output programs using
2

---

AlphaVerus
To demonstrate A phaVerus, we consider Dafny (Leino, 2010) programs as the source domain, since the Dafny lan- guage has been around for over a decade and has accumu- lated reasonable amount of code. We run AlphaVerus to automatically collect the DARNY2VERUS-CCLLLFFTTT a dataset of trajectories containing translated programs, er- ror corrections, and critique examples based on the source dataset Dafny Bench (Loughridge et al., 2025)-a dataset of 562 programs of varying difficulty. Finally, we evaluate the AlphaVerus pipeline by using the resulting data as few-shot exemplars for the downstream task of formally verified code generation: generating complete, formally verified inaplementationn-inllleeee and proof annotations- given numan-writted specifications Formally verified code generation is a significant step over concurrent work that focuses solely on the simplified, artifi- cial setting of generating proof annotations for correct pre- written code (Yang et al., 2024; Chen et al., 2024). We show Al AlphaVerus enables Llama-70B to successfully gener- ate verified solutions to 33% of HumanEval- HumanEval- VerruVerus Contributors, 2024), outperforming GPT- 4o-based methods. Furthermore, through ablations, we es- tablish the necessity of each component in Al AhaVees.
implementation conforms to the specifications. A verifier e(ys, yr, vr) - {0 uses the proof to statically check that the implementation meets the specification for all possi- ble inputs, returning 1 if the program is correct with respect to y, and 0 if verification fails. Upon failure, the verifier additionally returns a set of messages {mI,.... mM } con- taining the number of verified statements, the number of errors, and localized error messages (e.g., see Figure 2).
Misaligned specs and implementations. The specifica- tions themselves are not verified, as they represent the de- veloper's 's intended behavior. Therefore, it is critical that the specifications accurately reflect the desired input-output be- havior for all possible inputs. We use the term misaligned to refer to situations in which the specification does not reflect the desired input-output behavior. This includes misalign- ments between the specification and the developer's intent or the implementation, which can occur due to language features that cause programs to pass the verifier trivially (e.g., using "assume ( (false) ").
both algorithmic code
(The
Formally verified code generation. Our goal is to develop model that generates formally verified code given a spec- ification. Specifically, (yr, yp) G (ys; c, 0), where G(:) is generation algorithm such as sampling from language model with parameters 0, and the model generates both an implementation y/ and proofs yP given a specification ys and any additional context c. The goal is for the resulting code to verify, i.c., u(ys, yr, yp) 1.
In summary, our contributions are five-fold: (1) We pro- pose AlphaVerus, a novel self-improving framework for generating formally verified code; (2) We present a novel combination of tree search and refinement that improves over time; (3) We propose a novel critique phase, which has to our knowledge the first neural method that can improve the quality of specifications without test cases; (4) We in- troduce a new dataset containing formally verified Verus programs, along with error pairs; and (5) We demonstrate the effectiveness of our approach, evaluating its formally ver- ified code generation abilities and ablating its components. In particular, A AlphaVerus is the first method to achieve non-zero formally verified code generation performance on verified version of HumanEval (Chen et al., 2021), thus establishing a starting point for code generation models that generate increasingly complex- trustworthy-code.
Bootstrapping formally verified code generation. A prac- tical goal is perform formally verified code generation in a mainstream language, such as Rust code verified with the Verus verifier (Lattuada et al., 2023). However, doing so raises a technical challenge: it is infeasible to train a model on (ys, y1, yr) examples since few examples ex- ist. We refer to this as a bootstrapping problem, since we need to create an initial generation model (that we may subsequently improve) without any training data. Next, we describe Al AlphaVerus, framework for bootstrapping verified code generation model by translating from a more resource-rich language.
2. Formally Verified Code Generation
3. AlphaVerus
Our goal is to develop model that generates formally ver- ified code in a real-world programming language, which we refer to as formally verified code generation. Next, we provide background and then introduce AlphaVerus.
To generate verified code in the absence of training data in our target language (Verus), we propose to iteratively trans- late programs from higher-resource domain into Verus. Each iteration collects data by exploring candidate trans- lations, refining them with a novel tree search, and then filtering out misaligned programs. Finally. we use the data to enable a verified code generation model (via few-shot learning), and evaluate the model plus the tree search on the downstream task of verified code generation: generating verified code and proofs given held-out test specification.
Formal verification of code. Formal verification ensures that a program adheres to a formally defined specification of its intended behavior. As illustrated in Figure 2, formally verified code typically consists of three components: (1) formal specifications ys defining the expected input-output behavior; (2) code implementation yr intended to satisfy the specifications; and (3) proof yp demonstrating that the
3

---

AlphaVerus
Specification
Generator
Code + Proofs
spec is_prime(n: requires n forall|f: nat
bool {
wut while f <
Idivides(f,
Invariant
1,
1o g: u64
64 =>> Idivides 9, 1
Error Messages
Proof Annotations
Verifier
fnvarfant satisffed
asserti uisertidvvidestt, 5133
Toratlig: u84) 1 aa ieividen 1),
errort aborting das to previous arror verificatton results:t verifled,
or
Figure 2: Example of formally verified code generation. Given specification, A. AlpphVerus generates the corresponding code and proof. The verifier checks the proof and provides either verification success or detailed error messages.
3.1. Translation
Refinement with Treefinement. Having verifier opens the possibility of refining candidate programs into verified ones by providing detailed feedback, including unverified func- tions and specific errors like overflows, unsatisfied condi- tions, and syntactic mistakes (e.g.. Figure 2). While human programmers often use such feedback for iterative correc- tions, naively providing LLMs with incorrect solutions and feedback often fails produce improvements. Our key in- sight is that verifier feedback induces an implicit ordering of solutions based on verified functions and error severity. This ordering lets us extend common refinement techniques by framing refinement as a tree search over the space of refined programs, which we call Treefinement.
A1 AlphaVerus translates programs using three-stage pipeline consisting of exploration, refinement, and critique. The exploration stage translates source programs into can- didate Verus programs, The refinement stage repairs the programs using a novel tree search over program refine- ments. The critique stage uses suite of models discard flawed specifications and implementations that could de- grade future iterations. The pipeline iterates, creating self-reinforcing cycle where verified programs and refine- ment trajectories improve the models' capabilities, enabling translation of increasingly complex programs. The result is a growing synthetic dataset of progressively more complex and reliable Verus programs. The complete algorithm is listed in Algorithm and visualized in Figure 1.
Specifically, the refinement stage takes syntactically cor- rect but unverified candidate translations (VI,... ykr and performs a tree search to discover verified programs. Each node in the tree contains an imperfect program and its asso- ciated errors, (y, e(y)). Nodes are expanded by invoking a refinement model:
Exploration. Given source program x (e.g., a Dafny implementation, specification, and proofs), exploration uses a model to generate candidate target (i.e., Verus) programs:
fyn,...,ye) ~ Gerplore ar; D(9) 1-
(1)
tu.....,y% 3/3 Grefine (v. (y.e(y); (-.
(2)
where G is a generation algorithm (e.g., LLM sampling) that is given the source and set of (source, target) examples D. Initially, D has a few hand-written examples.
where ((9) "-o' is set of (program, error, correct program) examples, initially containing a few hand-written examples.
Given node scoring function (gy) IR that is used to prioritize nodes, we can search over the space of program refinements with a tree search algorithm that selects and expands nodes, such as breadth-firse or depth-first search.
Any generated (source, verified program) pairs are placed in a candidate set, C, that will be passed the filtering stage. If candidates verify for source x. candidates that are syntactically correct proceed to refinement. Intuitively, this stage serves as initial "exploration", in that it generates a set of candidates that may eventually be refined and filtered into verified programs in the later stages. Unlike other methods of bootstrapping (Zelikman et al., 2022; Lin et al., 2025) that discard anything but correct solutions, we use both syntactically correct programs and fully verified programs for further improvement, expanding the learning signal.
We develop symbolic scoring function based on the num- ber of (un)verified functions, errors, and warnings:
s(y) Tiver ()) (3
(y) + (t)
where (y)) is the number of verified functions in y. nen (y) and nawm (1) are the counts of errors and warnings from the verifier for the node's 's program y. a and B are

---

AlphaVerus
hyperparameters controlling the penalties for emrors and warnings, respectively. Intuitively, programs that are closer to a verified program have higher scores, with proximity determined by the proportion of verified functions, resolved errors, and resolved warnings. Upon generating a verified program, the program's 's search trajectory is added to a can- didate set C,, and the new (source, program) pair to the candidate set C' that is passed the critique stage.
to generate simple and often trivial solutions-such as re- turning an empty array-that satisfy the specifications, i.e., (yI, vP) Geeploit (us: Desplor) where is a generated specification, yr,yp an implementation and proof, and D
exploit contains (specification, implementation-prooff ex- amples. If such simple solutions pass verification, it indi- cates that the specification is flawed, and the corresponding translation discarded. This includes subtle forms of mis- specification; for instance, on tasks requiring array manip- ulation, the specification may omit conditions on the array length, resulting in trivial solutions.
Treefinement extends two kinds of prior methods into new search over program refinements. First, refining LLM outputs is a common technique (Madaan et al., 2023; Kamoi et al., 2024), but not within a tree search. On the other hand, tree search developed in step-by-step mathematical problem solving involves appending solution steps rather than refining a full program (Wu et al., 2024). Our approach specifically addresses the non-local nature of error fixes.
dellvimprovemnnt. Finally, the newly generated programs and a subset of the error trajectories are added to a pool of data that is used by the translator, refinement, and critique models in the next iteration. In this sense, the models "self- improve" given access the Verus environment, so long as the generated examples are useful exemplars.
Although Treefinement can use any tree search algorithm, we use REBASE (REward BAlanced SEarch) (Wu et al., 2024). REBASE allocates an exploration budget by sam- pling nodes from a distribution determined by the node scores at the current depth, providing an effective balance of exploration and exploitation. The search continues until it finds verified program or reaches maximum depth.
Formally, for exploration, we create new pool of examples,
D -D u D
where De-y consists of the (source, program) candidates C' that were collected during exploration and refinement, and that additionally pass the critique stage.
Critique. Synthesized specifications are the one part of the translation pipeline that lacks formal guarantees, which can result in a mismatch between the intended and actual functionality of generated programs. Furthermore, in a few degenerate cases, there can be mismatch between the spec- ification's 's intent and the program's implementation, since Verus has features that can result in trivial programs passing the verifier (e.g., assume (false)) ). These can lead to reward hacking, causing a snowballing effect when used as exemplars in future iterations. Hence, we propose a three- part approach for filtering out such misaligned programs: rule-based model, a comparison model, and an exploit model.
For refinement, we create a new pool of examples using the successful trajectories C, collected during refinement. Namely, we keep those trajectories whose final program passes the critique stage, and pair each intermediate program y and its errors with the final program y', i.e.,
D = (y, 8/) is an ancestor of s/), (4)
and set D ((++)) = Di U DD
Similarly, for the exploit model, we add (specification, pro- gram) exploits that pass the verifier into ((++)) to be used by the exploit model in the next iteration. Table 4 sum- marizes the components, feedback sources, models, and generated synthetic data at each stage.
The rule-based model receives generated program y. and detects if y uses a Verus feature which leads to trivial program. Since there are a relatively small number of such features, and these features can be detected through string matching, it suffices to use a list of hand-coded filters. This includes checking for assume (false), "# [verifiee fier:ffrr:: :external]" and trivial preconditions.
To use synthetic data as in-context exemplars, we employ a stochastic few-shot sampling approach. Specifically, each time a generator called, we randomly sample & examples from its respective data pool. This method reduces the com- putational cost associated with fine-tuning large models and, as shown in results, enables other models to leverage the data pool to improve their performance without any training. Nevertheless, fine-tuning models and developing learning objectives remain interesting future directions.
The comparison model [x, y) receives source input x and a program candidate y. and evaluates whether the specifica- tions and algorithms used in the candidate match those from the source in intent and structure. In practice, we prompt a model to generate multiple evaluation sequences and reject an output if at least sequences indicate rejection.
Source domain: Dafny.
As our initial source domain, we consider Dafny- a language that follows a similar paradigm to Verus and has been in use for over a decade, resulting
The exploit model is an adversarial approach that leverages the feedback from Verus. We use a generator prompted
5

---

AlphaVerus
in a larger of available data. We DafnyBench
Translation Success (%)
(Loughridge al., 2025), dataset of 562 Dafny programs.
Translation Success
Translating Dafny programs to Verus presents several chal- lenges due to two major differences: 1. Language Con- structs: Significant differences exist in supported features,
20
data types, and the design the underlying verifier, render- ing direct translations infeasible. Proof Requirements:
10
Verus imposes more rigorous proof obligations. such as overflow checks, making proofs harder to verify.
Iteration
Figure 3: Programs translated over iterations. The trans- lation success rate consistently improves over iterations.
3.2. Downstream Evaluation
After generating high-quality synthetic data in the form of formally verified Verus programs and error-feedback- correction triples, we use the data to enable model that performs formally verified code generation. Unlike prior work that requires L.LMs to fill proof annotations in existing code and specifications (Loughridge et al., 2025; Yang et al., 2024; Chen et al., 2024), we evaluate our models on the more challenging task of generating both the code and the proofs given only the specifications.
Datasets. We evaluate on verified versions of the MBPP and HumanEval datasets. In particular, MBPP-verified is sourced from (Yang et al., 2024; Misu et al., 2024) and con- tains 78 programs from the original MBPP dataset (Austin et al., 2021). HumanEval- -eruus sourced from a concur- rent open-source effort (The HumanEval- -eruus Contribu- tors, 2024) to translate existing HumanEval programs to Verus. For brevity, we refer to HumanEva 1 and MBPP as their respective verified versions throughout this paper.
We use two-part approach consisting of exploration and Treefinement. During exploration, given a specification ya. we generate i candidate programs (y()) ( If any candidate passes verification, we consider the task solved. Otherwise, we initialize Treefinement with the candidates and run it until we obtain a verified solution or reach max- imum number of iterations. This can be seen generator that uses the collected data as source of few-shot exem- plars, (UI, yP) G(ys; Dy. Dy-rg'), which means gener- ating an implementation and proofs using a language model prompted with a subset of the collected verified programs Dy and a test specification ys. followed by Treefinement with the collected refinement examples Dy-wy'
Baselines. Our primary evaluation is performed on verified code generation. Since no existing baselines exist for the task, we use few-shot variants (Listing C) of base models. We tried our best to adapt Vutu (Yang et al., 2024) to verified code generation, but due to the complexity of its hand-written prompts, we were not able to achieve non- trivial performance. Hence, we compare AlphaVerus on the MBPP proof annotation task against SAFE++ (Chen et al., 2024) and AutoVerus (Yang et al., 2024).
We refer readers to Appendix A.2 for more details.
5. Results and Analysis
4. Experimental Setup
AlphaVerus translation success monotonically in- creases. Figure 3 shows the number of successful trans- lations over each iteration. We see a steady increase the number of translations as the iterations increase. The results indicate that A AlphaVerus learns translate and gener- ate more complex programs over iterations. Altogether, A AlphaVerus translates around 45% of DafnyBench into Verus programs that are verified by Verus and aligned ac- cording to the critique models. Listings 2, 3, and in the Appendix show example translations.
Generators. We use LLaMA-3.20 1-70B for translation experiments and additionally evaluate LLaMA-3. 11-88, Qwen- 32B, and GPT-4o 4o for downstream tasks. The ex- ploration phase uses k 256 samples, while tree search uses breadth 32 and maximum depth 8.
Translation. We use DafnyBench consisting of 562 pro- grams as our source domain Drre for our translation experi- ments. The exploration model Gezplore is initialized using Verus syntax file and 5 examples from the Verus repository.
The exemplars generated during the translation process are collected into the DAFNY VEEEEE-COLLEUCEEEEEE 247 translated programs, 102 enror trajectories, and 579 exploit pairs. We use these exemplars for downstream tasks.
Downstream Evaluation. We evaluate formally verified code generation, where models must generate both an im- plementation and proof annotations given specification. We measure Pass K, where success requires at least one correct solution of the K generated programs.
totaling
AlphaVerus enables verified code generation. Table I shows the verified code generation performance for the AlphaVerus model obtained from the final translation
6

---

AlphaVerus
70
Exploration Tree Search
60
Accuracy
Score
50
Exploration@32
40
Exploration@256
30
AlphaVerus
64
128
192
256
320
384
448
512
0
2
3
4
5
6
Number of Generations
Iteration
Figure 4: Treefinement vs. exploration (HulanEval)), Treefinement leads to jump in performance that cannot be obtained by additional parallel sampling (exploration).
Figure 5: Translation iteration (x-axis) vs. downstream task performance on HumanEval (y-axis). Performance of pass @ 32 continues to improve, with pass @ 256 leveling off.
Method
HumanEval
MBPP
trivially verified but incorrect implementations. We observe snowballing effect where this behavior spreads across all programs (see Figure 6). While such cases can be disal- lowed done by our rule-based critic model, find more complicated reward hacking instances, such as incomplete specifications and degenerate translations (detailed in Fig- ure 7). The results show the need for our 3-model critique phase for preventing reward hacking.
Baselines
GPT-4o
27.1% %
35.9%
Llama 3.1 70B
11.8%
26.9%
Ablations (Treefinement Variants)
Single-Turn Linear Self-Refine
29.4%
61.5%
Multi-Turn Linear Self-Refine
29.4%
62.8%
Best-First Search
28.2%
61.5%
Treefinement outperforms linear refinement. We com- pare Treefinement against standard refinement that refines linearly, either by performing step of refinement across multiple parallel branches performing several steps of refinement across branches. Using equivalent generation budgets, we adjust the breadth and depth parameters accord- ingly. We also evaluate the best-first search as a bascline. As seen Table 1, methods improve upon initial ex- ploration, demonstrating Treefinement's compatibility with various search algorithms, and tree-search based refinement outperforms linear refinement. For the tree search, using REBASE outperforms the best-first search. Also note that the linear refinement variants are special cases of REBASE (depth = with large breadth, and temperature = oo).
AlphaVerus (Llama 3.1 70B)
Exploration
27.1% %
59.1%
+ Treefinement (Rebase)
32.9%
65.7%
Table 1: Verified code generation performance on the HumanEval and MBPP benchmarks (pass @ 226).
iteration. A1 Alphaveus leads to a substantial increase over its underlying Llama 3.1 70B model and a prompted GPT- 40 model. Moreover, Treefinement leads to an additional increase in performance over the exploration stage. Listings and 6 show example generations. Next, we analyze the impact of the various components in AlphaVerus.
AlphaVerus exemplars transfer to other models. key advantage of AlphaVerus is its ability transfer learned exemplars without model weight updates. Concretely, we use the exemplars collected during A AlphaVerus's translation phase, which used Llama 3.1 70B (i.c., the DARNYVVERUS-COLLECTI
Treefinement leads to jump in performance. We eval- uate the effectiveness of tree search compared to further scaling the parallel sampling (exploration) budget without refinement. Figure shows the percentage of solved prob- lems versus the generation budget for both approaches. Tree- finement leads to a substantial jump performance over exploration. Notably, exploration plateaus while tree search continues improving as the generation budget is increased.
to enable verified code generation on various models using the same few-shot prompting strategy outlined in $3.2. Table shows suc- cessful transfer both smaller and larger models, yielding significant improvements in verified code generation. No- tably, set using GPT-4o but without finetuning.
state-of-the-ar on both HumanEval,
Critique is crucial for preventing reward hacking. With- out the critique phase, our analysis of 100 DafnyBench examples reveals the model learns to game the verification system by using a assume ( (fal false) statements, leading to
AlphaVerus enables strong proof annotation. Unlike prior works that focus on the proof annotation task (gen-

---

AlphaVerus
HumanEval
Llama 8B Few Shot DARNY2VEUSS-COLLECTT
11.8%
18.8% %
Number of Transiations
Qwen-32B Few Shot
14.1 %
DAFNV2VERUS-COOLLECTO
27.1 %
GPT-4o Few Shot
27.1% %
37.7% %
Total Number of Translations Correct Number of Translations
Table 2: Transfer of
to other
language models without finetuning. All models show sig- nificant improvements over their few-shot variants.
Reward Hacked Solutions
Iterations
MBPP
Figure 6: Impact of removing the critique models. Without filtering mechanisms, the model learns exploit verification by increasingly using assume (false) statements. This snowballing effect shows the importance of critique models in preventing reward-hacked solutions.
SAFE
59.0%
Auto 65.4%
AlphaVerus 75.7% %
Table 3:
Comparison of proof annotation generation tasks against baselines on the MBPP dataset.
Debug Statement
Trivial Specs
Trivial Specs reaitee
de
retirn
cepts learned over iterations, showcasing how the model starts by learning how to translate basic syntax, followed by numeric algorithms, and array-related concepts.
Statemert
Debug Statement
Trivial
Foe Preatins
Further, Listing 2, 3, 4 show example Dafny-to- Do-russo-Verus Verus trans- lations from AlphaVerus, indicating that AlphaVerus is capable of complex translations often spanning mul- tiple specifications, helper functions, and proof annota- tions reaching over 100 lines of Verus code. For for- mally verified code generation, Listing 1 shows exam- ple generated by AlphaVerus; more examples showcas- ing A1 Allphaeeru rus's 's ability to generate multi-function pro- grams, and non-trivial lemmas are shown in Appendix D.2.
Figure 7: Illustration reward hacking without the critique models. In particular, the agent first learns to use debug statements and uses them continuously. After fixing, it learns other hacks such generating trivial specifications or explor- ing rare debug statements such as allowing infinite loops.
erating proofs given correct code), our method tackles the harder task of cormally-verified-codd generation, where the model must generate both code and proofs. Despite this, we outperform SAFE (Chen et al., 2024) and Auto Verus (Yang al., 2024) by 17% and 10% respectively on the proof annotation task (see Table 3). This is notable given that Veruu was specifically designed for this task while us- ing significantly more engineering effort and task-specific prompts. Moreover, we achieved these results using just 562 Dafny programs and an open 70B model, compared to SAFE's month-long GPT-4 invocations and training on thousands of programs. Overall, the results point to the ef- fectiveness of A AlphaVerus, along with its flexibility and data efficiency. Appendix D.1 contains additional details.
Finally, in Figure 9, we show that for lower budgets, us- ing smaller models such as LLaMA-3. 1-8B performs bet- ter than larger LLMMA-3. 1-70B the same cost. How- ever, LLaMA-3 1 1-70B achieves higher asymptotic perfor- mance, analogous to prior work (Wu et al., 2024).
6. Related Work
Automated Formal Verification. Automated formal ver- ification has long-standing history interactive theo- rem provers like Coq (Coq Development Team, 2020), Lean (Lean FRO), and Isabelle (Isabelle), with approaches generating step-by-step proofs (Redmon & Sanchez-Stemt 2016; Kaliszyk et al., 2018; Polu & Sutskever, 2020; First et al., 2020; Lu et al., 2023; Li at., 2024). While successful for mathematical theorems, application to code verification remains limited to existing project theorems (First et al.,
Other experiments. We manually inspect translations from each iteration of AlphaVerus to understand what the model learns over iterations. Figure 8 shows the new con-
8

---

AlphaVerus
Listing I: AlphaVerus implementation of the unique sorted function, which removes duplicates from a sorted vector.
Function signature upesitication (given to fr. ur prriqueesartedde Vepci399) fresuler Veoci325)
suquites
forallit: int, di inel 0 de
s.len m*> elil et5l.
forallli: lat, 11 intl 0 <e 1 < resuit.iond an> resuit(s] resulti31. lit: int1 A|jsuto] 0 ie i result.lent aay containn tresult [5]), forellli; inti Atstriggen w[-1) oe 1 alle wes resulte containn [i]ll,,
7
8
Model generation starts here let not result Vectsnew()
11
1s: not 1: usize -
shile 6.
Invariant
14
Ien <" 1y
15
1 <- len
16
foralligs intil
result, (e max =8-contai interall 1 intl),
forallig: intl 3.4.4 mn chid as ins] std int),
19
if -- 3 alt] 1- +lf re001
20
22
1:
23
24
prost
sesert (foralll4: int, 3: int 1 recuit.isnt) ressit(1] resoit(d)) by
26
ascert (torallii: int, 1: int1 0 <- s.len0 ->> s3(1] 5013))7
27
assert (resalt. len =- s.len()
(resait9.
int 59.1en() intly (b.to_moltiees:11
assect
30
31
32
result
2023) or simple properties (Lohn & Welleck, 2024). Inte- grating language models with verification languages such Dafny (Leino, 2010; Sun et al., 2024a; Loughridge al., 2025) and F* (Swamy et al., 2016; Chakraborty et al., 2025) face roal-world applicability challenges.
sampling strategies. Unlike these sample-and aanple-and-flter strate- gies, AlphaVerus self-improves using different feedback sources, with data collected from multiple modules.
We refer readers to Appendix B for a more detailed discus- sion of related work.
Rust Verification & Concurrent Work. Verus (Lat- tuada et al., 2023) brings verification to Rust but suffers from data scarcity. Recent concurrent works address this through GPT-4 pipelines (AutoVerus (Yang al., 2024), requiring significant human effort) and dataset translation (SAFE++ (Chen et al., 2024), using month-long GPT-4 generation). AlphaVerus differs by using open mod- els, 100x less data, and introducing tree-search refinement with critique for verified code generation (implementation + proofs), outperforming their linear refinement strategies.
7. Conclusion
We introduced AlphaVerus, novel self-improving framework for generating formally verified code in main- stream programming languages. By leveraging iterative translation from a higher-resource language (Dafny) to Verus and utilizing verifier feedback through our Explo- ration, Treefinement, and Critique stages, AlphaVerus overcomes the challenges of scarce training data, reward hacking and the complexity of formal proofs. We hope that the methods proposed in our work, such the cri- tique models and treefinement, may evolve to handle more complex cases of reward hacking and search with LLMs. Our approach operates without human intervention, hand- engineered prompts, or extensive computational resources, yet achieves significant performance improvements on ver- ified versions of the HumanEval and MBPP benchmarks where prior methods fail. We also contribute new dataset of formally verified Verus programs, providing valuable re- sources for future research. A AlphaVe Sishaeeru Verus opens up new avenues for grounding code generation and developing trust- worthy Al-assisted programming tools.
Meta-generation strate- gies (Welleck et al., 2024) boost reasoning via parallel sam- pling (Wang et al., 2022: Aggarwal et al., 2023; Sun et al., 2024b), tree search (Yao et al., 2024; Wu et al., 2024), and refinement (Welleck et al., 2023; Madaan et al., 2023; Snell et al., 2025). Unlike previous methods that perform stepwise verification (Wu et al., 2024) with separate reward model, Treefinement combines different verification sources such as scalar values, language feedback and refines complete programs, addressing the non-local nature of error fixes.
Inference-Tine Strategies.
Self-Improvement in LLMs. Recent work explores im- proving language models through self-generated data and external feedback (Zelikman et al., 2022; Wang al., 2025; Hosseini et al., 2024), using expert iteration or rejection

---

AlphaVerus
Acknowledgements
Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M. Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavar- ian, M., Winter, C., Tillet, P., Such, F. P., Cummings, D., Plappert, M., Chantzis, F., Barnes, E.,, Herbert- A., Guss, W. H., Nichol, A., Paino, A., Tezak, N., Tang, J., Babuschkin, I., Balaji, S., Jain, S., Saunders, W., Hesse, C., Carr. A. N., Leike, J., Achiam, J., Misra, V., Morikawa, E., Radford, A., Knight, M., Brundage, M., Murati, M., Mayer, K., Welinder, P., McGrew, B., Amodei, D., McCandlish, S., Sutskever, I., and Zaremba, W. Evaluating large language models trained on code. https: http//axivvv.// wwwpiiioorra/aaa wttpo//////a...aeeeeeeeeeeeee//a http///a........//// http:/2217000337.1. 03374 2021.
We thank Convergent Research and the OpenAl Researcher Access program. We also thank Alex Bai, Jay Bosamiya, Edwin Fernando, Md Rakib Hossain, Jay Lorch, Shan Lu, Natalie Neamtu, Bryan Parno, Amar Shah, Elanor Tang for their contributions to the version of the HumanEval-Veruu benchmark we used in our experiments. This work was funded in part by gift from VMware, the Future Enterprise Security initiative at Camegie Mellon CyLab (Futu prise @ @CyLa.) and AFRI, and DARPA under Agreement
FA8750-24-9-1000.
Impact Statement
Chen, T., Lu, S., Lu, S., Gong, Y., Yang. C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., Yang. F., Lahiri, S. K., Xie, T., and Zhou, L. Automated proof generation for Rust code via self-evolution, 2024. URL https: //arxiv.org/aallllb hbwg///bs/s/aa 220...151...55
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none which we feel must be specifically highlighted here.
Chen, X., Lin, M., Schärli, N., and Zhou, D. Teaching large language models to self-debug. arXiv preprint arXiv:2344.05128 2023.
References
Aggarwal, P. Madaan, A., Yang. Y., and Mausam. Let's sample step by step: Adaptive-consistencyy for efficient reasoning and coding with LLMs. In Bouamor, H., Pino, J., and Bali, K. (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 12375-12396, Sin- gapore, December 2023. Association for Computa- tional Linguistics. doi: 10.118663/11/0023emmlpp 761. URL https: https///caaatthoooooo ott/2023.....0033 emnlp-main. 761/.
Chern, I., Chern, S., Chen, S., Yuan, W., Feng, K., Zhou, C., He, J., Neubig, G., Liu, P., et al. FacTool: Factuality detection in generative Al-a a tool augmented framework for multi-task and multi-domain scenarios. arXiv preprint MiXi:2307.13558 2023.
Coq Development Team. The Coq Proof Assistant. https: //coo.iiniaa ftr,iiaa.fr//0000 f02.
Denison, C., MacDiarmid, M., Barez, F., Duvenaud, D., Kravec, S., Marks, S., Schiefer, N., Soklaski, R., Tamkin, A., Kaplan, J., Shlegeris, B., Bowman, S. R., Perez, E., and Hubinger, E. Sycophancy to subterfuge: Investigating reward-tampering in large language models. https: / //arxiv.org/////. abs 2406 ......00000 101 62, 2024.
Akyürek, A. F., Akyürek, E., Madaan, A., Kalyan, A., Clark, P., Wijaya, D., and Tandon, N. RI4f: Generating natural language feedback with reinforcement learning for re- pairing model outputs. arXiv preprint arXiv:2305.08844 2023.
Austin, J., Odena, A., Nye, M., Bosma, M., Michalewski, H., Dohan, D., Jiang, E., Cai, C., Terry, M., Le, Q- et al. Program synthesis with large language models. https:/ aarxivvv org/ abs/ 2200221.... 07732, 2021.
Elgedawy, R., Sadik, J., Dutta, S., Gautam, A., Georgiou, K., Gholamrezae, F., Ji, F., Lim, K., Liu, Q., and Ruoti, S. Occasionally secure: A comparative analysis of code generation assistants. https: www.a.iivoooooo...o..aaaooao abs/ 2402. 00680 9, 2024.
Chakraborty, S., Ebner, G., Bhat, S., Fakhoury, S., Fatima, S., Lahiri, S., and Swamy, N. Towards Neural Synthesis for SMT-assisted Proof-Oriented Programming. In 2025 JEEE/ACM 47th International Conference on Software Engineering (ICSE), pp. 13-25, Los Alamitos, CA, USA. May 2025. IEEE Computer Society. doi: 10. 10.1000/CSE5554472225.0000 http::://aa..eeeeccopteeeerrr 2025. 00002.
First, E., Brun, Y., and Guha, A. Tactok: semanties- aware proof synthesis. Proc. ACM Program. Lang., (OOPSLA), Nov 2020. doi: 10. 10.1145/3428299, URL https://doi. 2t11//..2.0.r11111114/422222992
URL org/
First, E., Rabe, M., Ringer, T., and Brun, Y. Baldur: Whole- proof generation and repair with large language mod- els. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/ESE
10.
Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N.,
10

---

AlphaVerus
2023, pp. 1229-1241, New York, NY, USA, 2023. Asso- ciation for Computing Machinery. ISBN 97984007032700. doi: 10. 10.1145/3611644333662222 URL atttps://dol:
Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., and Hawblitzel, C. Verus: Verifying Rust programs using linear ghost types. Proc. ACM Program. Lang., 7(00PSLAI), April 2023, doi: 10. 145/3586667 URI.https. / /toi///o.//// org/10. 1145/ 01553556037
Gou, Z., Shao, Z., Gong, Y. Shen, Y., Yang, Y., Duan, N., and Chen, W. Critic: Large language models can self-correct with tool-interactive critiquing, 2024. URL https: / //tp/aaavvv///////////eeeeaaaav. www.iii.org.aa..e.oooooeoooeeeee wwtp///g/////ooooeo 2305. 11738.
Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J., Padon, O., and Parno, B. Verus: A practical foundation for systems verification. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), November 2024.
Hendler, J. Understanding the limits of Al coding, Science, 379(6632):548 -58, 2023.
Hosseini, A., Yuan, X., Malkin, N., Courville, A., Sordoni, A., and Agarwal, R. V-STaR: Training verifiers for self- taught reasoners, 2024. URL httpstts://axxii
Lean FRO. Lean theorem prover. leanprover. www.rooeergittu........ www.ggithhbiooo
https://
abs/2402.
Leino, K. R. M. Dafny: An automatic program verifier for functional correctness. In Proceedings of the Conference on Logic for Programming. Artificial Intelligence, and Reasoning (LPAAR), 2010.
Isabelle. de/.
Isabelle. https://isabelle tum.
Jesse, K., Ahmed, T., Devanbu, P. T., and Morgan, E. Large Language Models and Simple, Stupid Bugs. In 2023 JEEE/ACM 20th International Conference on Mining Software Repositories (MSR), pp. 563-575, Los Alamitos, CA, USA. May 2023. IEEE Computer Society. doi: 10.1 02110//MSR3993332223.000000 https: http://bi...eeecooopprrtrroiiaii 001-11199/S5590733 2023. 00082.
Li, R., Allal, L. B., Zi, Y., Muennighoff, N., Kocetkov, D., Mou, C., Marone, M., Akiki, C.,, Li, J., Chim, J., Liu, Q. Zheltonozhskii, E., Zhuo T. Y., Wang, T., De- haene, O., Davaadorj, M., Lamy-Poirier, J., Monteiro, J., Shliazhko, O., Gontier, N., Meade, N., Zebaze, A., Yee, M.-H., Umapathi, L. K., Zhu, J., Lipkin, B., Oblokulov, M., Wang. Z., Murthy, R., Stillerman, J., Patel, S. S., Abulkhanov, D., Zocca, M., Dey, M., Zhang, Z., Fahmy, N., Bhattacharyya, U., Yu, W. Singh, S., Luccioni, S.. Villegas, P., Kunakov, M., Zhdanov, F., Romero, M.. Lee, T., Timor, N., Ding, J., Schlesinger, C., Schoelkopf, H., Ebert, J., Dao, T. Mishra, M., Gu, A., Robinson, J., Anderson, C. J., Dolan-Gavitt, B., Contractor, D., Reddy, S., Fried, D., Bahdanau, D., Jernite, Y., Ferrandis, C. M., Hughes, S., Wolf, T., Guha, A., von Werra, L., and de Vries, H. StarCoder: May the source be with you! https: http://axxivvooo orriiiiorrgaeeo 2205 061 61, 2023.
URL
Jimenez, C. E., Yang. J., Wettig, A., Yao, S., Pei, K., Press, O., and Narasimhan, K. R. SWE-bench: Can language models resolve real-world GitHub issues? In The Twelfth International Conference on Learning Representations, 2024. URL htttps://openreeee wtw.pperrrvieeeeee/eeooeee ferrmf id- CL-VTF8yNQM66
Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving- In Proceedings of the 32nd International Conference Neural Information Processing Systems, NIPS' 18, pp. 8836-8847, Red Hook, NY, USA, 2018. Curran Asso- ciates Inc.
Li, Y. Choi, D., Chung. J., Kushman, N., Schrit- twieser, J., Leblond, R., Eccles, T. Keeling, J., Gi- meno, F., Lago, A. D., Hubert, T., Choy, P., de Mas- son d' Autume, C., Babuschkin, I., Chen, X., Huang, P.-.., Welbl, J., Gowal, S., Cherepanov, A., Mol- loy, J., Mankowitz, D. J., Robson, E. S., Kohli, P., de Freitas, N., Kavukeuoglu, K., and Vinyals, O. Competition-level code generation with AlphaCode. Science, 17866624) 1092-1097, 2022. doi: 10.1 science.abyl 1558. URL https: :/tp:://www science. org/ prg/doi/ doi abs///b///////// / /t////1111111 1 wtt22//sciennc..ee. abq1158.
Kamoi, R., Zhang, Y., Zhang, N., Han, J., and Zhang, R. When can LLMs actually correct their own mis- takes? A critical survey of self-correction of LLMs. Transactions of the Association for Computational Linguistics, 12:1417-1440, 2024. doi: 10.1162/tacL. 1.00713. URL https: / http//occaacoooyoo.o/ org/ 2024. t.81-1.78.
Li, 7.,, Sun, J., Murphy, L.,, Su, Q. Li, 7., Zhang, X., Yang, K., and Si, X. A survey on deep learning for theorem proving. In First Conference on Language Modeling, 2024. URL https::///// htts:://pppeeeieeeeeeeee net/ forum? id=z HWWkk.
Langley, P. Crafting papers on machine lcarning. In Langley, P. (ed.), Proceedings of the 17th International Conference on Machine Learning (ICML 2000), pp. 1207-1216, Stanford, CA, 2000. Morgan Kaufmann.

---

AlphaVerus
Lin, H., Sun, Z., Welleck, S., and Yang. Y. Lean- STar: Learning interleave thinking and proving. In The Thirteenth International Conference on Learning Representations. 2025. http:: //pp/reeee.e...eee/e/eeee net/forund d=sow/550999000
Pearce, H. A., Ahmad, B., Tan, B., Dolan-Gavitt, B., and Karri, R. Asteep at the keyboard? Assessing the secu- rity of GitHub Copilot's code contributions. 2022 IEEE Symposium on Security and Privacy (SP), Pp. 754-768, 2021. URL. www.t:ttt/t......m /api..p..../ http://ppp...a..ate..ee.em semant cscholars org/ hespCCrruusDD 245220588.
Liu, J., Xia, C. S., Wang. Y., and Zhang. L. Is your code generated by ChatGPT really correct? rig- orous evaluation of large language models for code generation. In Thirty-seventh Conference Neural Information Processing Systems, 2023, URL https: //openrevien, htt.e/viiw..eee/orroeeeeeee wwr.m/ormmmmmmmmmmoommm htt.:/oooooimii1iiix0000000000
Peng. B., Galley, M., He, P., Cheng, H., Xie, Y., Hu, Y., Huang. Q., Liden, L.., Yu, Z.., Chen, W., et al. Check your facts and try again: Improving large language models with external knowledge and automated feedback. arXiv preprint arXiv:2302.12813 2023.
Lohn, E. and Welleck, S. miniCodeProps: A minimal benchmark for proving code properties. In Neurips Safe Generative AI Workshop 2024, 2024. URL https: //openrevieew.ne//formmm d
Perry, N., Srivastava, M., Kumar, D., and Boneh, D.
Do users write more insecure code with Al assistants? Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security CCS '23. ACM, November 2023. doi: 10. 10.1144/357661153623111 URL http: /ttt:://d.... http//xxx/xo/ doi. wttpooo.o.o......o.o.oo 1111/ 3 3623157.
Loughridge, C. R., Sun, Q., Ahrenbach, S., Cassano, F., Sun, Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., and Tegmark, M. DafnyBench: A benchmark for formal software verification. Transactions on Machine Learning Research, 2025. ISSN 2835-8856. URL https:// openreview net/ forum? ddyBgTVWccII...
Polu, S. and Sutskever, I. Generative language mod- cling for automated theorem proving, arXiv preprint arXiv:2009.03393 2020.
Lu, P. Qiu, L., Yu, w., Welleck, S., and Chang, K-- W. A survey of deep learning for mathematical rea- soning. In Rogers, A., Boyd-Graber, J., and Okazaki, N. (eds.), Proceedings of the 6lst Annual Meeting of the Association for Computational Linguisties (Volume I: Long Papers), pp. 14605-14631, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.18655/w122223.ccHooggg //aclanthology.orgg.ooooo
Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, Formal mathematics statement curricu- lum learning. arXiv preprint arXiv:2202.0133 2022.
Redmon, J. and Sanchez-Stern, A. Proverbot 9000 : Neural networks for proof assistance, 2016. URL https:
prrpi.semanticsee www..ecco......ooooosolll....... org/CorpusID: 11622595.
URL https: acl -ocel11i long. 887.
Madaan, A., Tandon, N., Gupta, P., Hallinan, S., Gao, I.., Wiegreffe, S., Alon, U., Dziri, N., Prabhumoye, S., Yang, Y., Gupta, S., Majumder, B. P., Hermann, K., Welleck, S., Yazdanbakhsh, A., and Clark, P. Self-refine: Iter- ative refinement with self-feedback. In Thirty-seventh Conference on Neural Information Processing Systems, 2023. URL https: htttpps://ppeeeeee http///ppeeeeeeeee//////ee net/forunt id- 1d-S37h0erQLB.
Rozière, B., Gehring, J., Gloeckle, F,, Sootla, S., Gat, I., Tan, X. E., Adi, Y., Liu, J., Sauvestre, R., Remez, T., Rapin, J., Kozhevnikov, A., Evtimov, I., Bitton, J., Bhatt, M., Ferrer, C. C., Grattafiori, A., Xiong, W., Défossez, A., Copet, J., Azhar, F,, Touvron, H., Martin, L., Usunier, N., Scialom. T., and Synnaeve, G. Code Ilama: Open foundation models for code. abs abs/2308..5 02.300...299,, 2024.
Misu, M. R. H., Lopes, C. V., Ma, I., and Noble, J. To- wards Al-assisted synthesis verified Dafny methods. Proceedings of the ACM on Software Engineering, (FSE):812 835, July 2024. ISSN 2994-970X. doi: 10.1145/3643763. URL http://dds doi wwt.ddd......og/....o1 1145/3643765.
Schick, T., Dwivedi- Yu,vedi-Yu,11. J., Dessi, R., Raileanu, R., Lomeli, M., Zettlemoyer, L.. Cancedda, N., and Scialom, T. Toolformer: Language models can teach themselves to use tools, 2023. URL 2302.04761.
Snell, C. V., Lee, J., Xu, K., and Kumar, A. Scaling LLM test-time compute optimally can be more effective than scaling parameters for reasoning. In The Thirteenth International Conference on Learning Representations, 2025. URL htwpt:ttp////eccm //tp::/s////peeeveew net forum? i 1d=4FWAwzzd2n.
Pan, A., Bhatia, K., and Steinhardt, J. The effects of reward misspecification: Mapping and mitigating mis- aligned models. In International Conference on Learning Representations, 2022. URL https:::: httpt:pssp///pereeee..... net/ forum? d=dYtwGWTL77e..
12

---

AlphaVerus
Sun, C., Sheng, Y., Padon, O., and Barrett, C. Clover: Closed-loop verifiable code generation. In Avni, G., Gi- acobbe, M., Johnson, T. T., Katz, G., Lukina, A., Naro- dytska, N., and Schilling, C. (eds.), AI Verification, pp. 134-155, Cham, 2024a. Springer Nature Switzerland. ISBN 978-3-031-65112-0..
Wu, Y., Sun, Z., Li, S., Welleck, S., and Yang, Y. An empirical analysis of compute-optimal inference for problem-solving with language models. https:// azxiv. abs 2408. 00724, 2024.
Yang. C., Li, X., Misu, M. R. H. Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S. Yang, F,, Zhou, Z., and Lu, S. Veru: Au- tomated proof generation for Rust code, 2024. URL https: aaaaaaiiiiiv..io owt.oo/g///...... abs 2409. 13082.
Sun. Z.,, Yu, L.., Shen, Y., Liu, W. Yang, Y., Welleck, S., and Gan, C. Easy-to-hard to-d generalization: Scalable alignment beyond human supervision. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, net/ forum?
Yao, S., Yu, D., Zhao, J., Shafran, I,, Griffiths, T. L., Cao, Y., and Narasimhan, K. Tree of thoughts: Deliberate problem solving with large language models. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS '23, Red Hook, NY, USA, 2024, Curran Associates Inc.
2024b. URL https:::: /ttps:////eer///ee id-qwgfh2fTeN.
Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat- Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoué, J.-K., and Zanella- Béguelin, S. Dependent types and multi-monade effects in F* 2016. ISBN 978-1-4503-3349-2.
Yuan, Z., Yuan, H., Li, C., Dong, G., K., Tan, C., Zhou, C., and Zhou, J. Scaling relationship on learning math- ematical reasoning with large language models, 2023. URL https: / arxiv. org aba 2aoba/2308.. 01825.
Team, Q. Qwen2.5: party of foundation models. ht attps: /qweelmm.mmmmmmmmmmm..mm.m//m gi tutt.uu..... htt.ol///////ooo.ooooooooooooo/t hwwloo////ee.//////. September 2024.
Zelikman, E., Wu, Y., Mu, J., and Goodman, N. D. STaR: Self-taught reasoner bootstrapping reasoning with reason- ing. In Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS '22, Red Hook, NY, USA, 2022, Curran Associates Inc. ISBN 9781713871088.
The HumanBvvll-Vrus Contributors.
HumanEval- Verus: Hand-written examples verified Verus code derived from HumanEval, 2024. URL https: //github.
wtwp://u..ccooccceeeeeeeeeeeeeee http:/uuuueefdnaatiioo.. numan-eval-ves git..
Zhang, K., Li, Z., J., Li, G., and Jin, Z. Self-edit: Fault- aware code editor for code generation. arXiv preprint arXiv:2305.0408/ 2023.
Wang, T., Kulikov, I,, Golovneva, O., Yu, P., Yuan, W., Dwivedi-Yu, J., Pang, R. Y., Fazel-Zarandi, M., Weston, J. E., and Li, X. Self-taught evaluators, 2025. URL https::///// http:///ppeerviieeeeee net/ forum? id=I7uCWGxVnI
Zheng, L., Yin, L., Xie, Z., Sun, C., Huang, J., Yu, C. H., Cao, S., Kozyrakis, C., Stoica, I., Gonzalez, J. E., Barrett, C., and Sheng, SGLang: Efficient execution struc- tured language model programs. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. https:: wwppreviee..eeee///// net/ forum?id=VgkaAn
Wang, X., Wei, J., Schuurmans, D., Le, Q., Chi, E., Narang, S., Chowdhery, A., and Zhou, D. Self-consistency im- proves chain of thought reasoning in language models. arXiv preprint arXiv:2203.1117. 2022.
Zhong, L. and Wang, Z. Can LLM replace Stack Over- flow? a study on robustness and reliability of large language model code generation. Proceddings of the AAAI Conference on Artificial Intelligence, 38(19): 21841-21849, Mar. 2024. doi: 2.11609aaai.vv88i1 30185. URL https://ojs. aaai. org/ in///i.dx.... pho.ALatt/artticle/vveee/////
Welleck, S., Lu, X., West, P., Brahman, F. Shen, T., Khashabi, D., and Choi, Y. Generating se- quences by learning self-correct. In The Eleventh International Conference on Learning Representations, 2023. URL https//////eeeeee..eeeeeeeeeee id=hH36 JJCDDDaO.
Welleck, S., Bertsch, A., Finlayson, M., Schoelkopf,
H., Xie, A., Neubig, G., Kulikov, I., and Harchaoui, Z. From decoding to meta-generation: Inference-time algorithms for large language models. Transactions on Machine Learning Research, 2024. ISSN 2835- 8856. URL httts::/ dd=eskgMcTbbl Survey Certification.
net/ forum?
13

---

AlphaVerus
A. Experimental Details
A.I. Translation
We use DafnyBench as our source domain Dare for our translation experiments. Starting with 782 programs, we filter to 562 by excluding those that verify without proof annotations. The exploration model Geaplore is initialized using Verus syntax file and 5 examples from the Verus repository.
A.2. Datasets
We evaluate on verified versions of the MBP? and HumanEval datasets. In particular, MBPP-verified is sourced from (Yang al., 2024; Misu et al., 2024) and contains 78 programs from the original MBPP dataset (Austin et al., 2021). HumanEva Morra--Vent --Veu is sourced from concurrent open-source effort (The HumanEval-Venns Contributors, 2024) to translate existing HumanEval programs to Verus. Since each task in HumanEval-Venut is typically implemented and verified using multiple functions, we split each program into individual provable functions, ensuring that all dependent functions needed are present. Specifically, we split 49 programs into 85 functions and evaluate methods on these 85 functions. We use a snapshot from November 4th, 2024 with commit hash 9bb. For brevity, we refer to HumanEval and MBPP as their respective verified versions throughout this paper.
A.3. Hyperparameters
We use consistent decoding parameters, with temperature set to 0.7, top-p set to 1.0 and max tokens set to 2048. For the translation step, we generate 256 examples per program in the translation phase. We set breadth and depth to 32 and 8 the treefinement stage. a is set 0.1 and / set to 0.03 as defined in Equation We set the rebase node sampling temperature to 0.1. We generate 32 samples for the comparison model and exploit model. We the same setting in both inference and translation. For stochastic sampling described in Equation 3.1, randomly choose k/2 examples from the pool of k exemplars. All sampling is done with a batch size of 32. We do not tune hyperparameters and use the conventional settings throughout. We use the "gpt-4o-2024-08-00 version for GPT-4o modal.
A.4. Contamination Analysis
Despite independent development of HumanEval and MBPP, we observe significant overlap between these datasets and DafryBench programs. To mitigate contamination in downstream evaluations, we employ GPT-4 for systematic filtering of collected exemplars. Specifically, we prompt GPT-4 with each collected exemplar paired against individual programs from HumanEval] al and MBPP, requesting the identification of similar programs. We generate independent evaluations per pair and flag contamination when similarity is detected in more than two evaluations. Flagged examples are excluded from the in-context examples during evaluation of the corresponding program. The prompt used is in Listing C.
Manual analysis confirms this approach significantly outperforms traditional n-gram analysis and aligns well with human assessment of contamination. We recommend future work adopt similar contamination detection methods rather than relying solely on n-gram analysis for program similarity. Notably, existing baseline methods for proof annotations in Verus (Yang et al., 2024; Chen et al., 2024) lack such contamination analysis.
A.5. Hardware and Software
We use L40S GPUs for inference. We use SgLang for inference (Zheng et al., 2024). We design a scalable and parallel version of the translation and inference stage, where each program is run on a separate node. We release the complete codebase and our DANNYV for reproducibility.
B. Related Work
Automated Formal Verification. Automated formal verification has a long-standing history in interactive theorem provers (Redmon & Sanchez-Stem,, 2016; Kaliszyk et al., 2018; Polu & Sutskever, 2020; First et al., 2020; Lu et al., 2023; Li et al., 2024), such as Coq (Coq Development Team, 2020), Lean (Lean FRO), and Isabelle (Isabelle). These approaches typically generate step-by-step proof statements for a given problem, with the theorem prover providing feedback on intermediate steps. While these methods have achieved significant success proving complex mathematical theorems, their application to formal verification of code is typically limited to theorems from existing projects (c.g., First et al. (2023))
14

---

AlphaVerus
or simple program properties (Lohn & Welleck, 2024) rather than end-to-end verified code generation. An alternative paradigm integrates language models with languages that offload proving to automated reasoning tools (e.g., SMT), including Dafny (Leino, 2010; Sun et al., 2024a; Loughridge et al., 2025) and F* (Swamy et al., 2016; Chakraborty et al., 2025), However, enabling verified code generation in these research languages may have limited applicability to real-world software and workflows.
Automated Formal Verification in Rust. In contrast, Verus (Lattuada et al., 2023) offers a verification framework for Rust, a widely adopted programming language. However, unlike in formal theorem proving or long-standing verification languages, there is a substantial lack of data for Verus. Two existing works, released during the development of AlphaVerus, Verus, attempt to overcome data scarcity. First, AutoVerus (Yang et al., 2024) prompts GPT-4 with a pipeline of hand-engineered prompts tailored specific errors and programs. This allows for refining some errors but requires human expertise to support new strategies through additional prompts. In contrast, our Treefinement method learns new refinement strategies automatically. Second, the concurrent work SAFE++ (Chen et al., 2024) proposes translating an existing Rust dataset to Verus and training generation and refinement models on the collected data. However, the translation process in Chen et al. (2024) was initialized with over a month of continuous generation from GPT-4, In contrast, AlphaVerus relies only on a single openly available model, without an expensive GPT-4 initialization. AlphaVerus also incorporates a new tree-search refinement strategy that outperforms the linear strategy used in SAFE++, and a eritique phase to ensure the generated specifications are high quality. These innovations contribute to better results, despite our method using open models and 100 times less data, Finally, these two existing works study the simplified task of proof generation, while study the more general setting of verified code generation: generating the implementation and its proofs.
Inference-Time Strategies. Recent studies have shown that increasing inference-time compute can improve performance in reasoning, mathematics, and code generation via meta-generation strategies (Welleck et al., 2024) such as parallel sampling (Wang et al., 2022; Aggarwal et al., 2023; Sun et al., 2024b), tree search (Yao et al., 2024; Wu et al., 2024), and refinement (Welleck et al., 2023; Madaan et al., 2023; Snell et al., 2025). Our Treefinement algorithm can be viewed as a hybrid meta-generator that combines tree search and refinement, following initial parallel sampling (exploration). A variety of tree search methods generate one step of mathematical solution at a time, with a verifier guiding the search process by assigning score to the current state (Wu et al., 2024). In contrast, Treefinement uses verifier feedback on the complete solution, modeling tree nodes as full programs and edges as refinement steps. Our strategy addresses the non-local nature of error fixes, and does not need an additional trained scoring model.
Various refinement strategies use external feedback from knowledge bases (Peng et al., 2023; Chern et al., 2023), code interpreters (Chen et al., 2023; Zhang et al., 2023), tool outputs (Gou et al., 2024; Schick et al., 2023), or separately trained reward models (Akyürek et al., 2023). Our Treefinement algorithm uses a diverse set of feedback sources, including scalar and binary values, language feedback, and an exploit model. Moreover, whereas prior methods typically operate in a linear fashion-iee., starting with an output and repeatedly refining it-our approach structures refinement as a tree search. This allows for prioritizing certain branches of refinement, which we find perform better.
Self-Immpovement in LLMs. Various algorithms aim to improve a language model using data generated by the model along with an external feedback source (Zelikman et al., 2022; Wang al., 2025; Hosseini et al., 2024), which is colloquially termed self-improvement. Common approaches rely on variants of expert iteration or rejection finetuning (Polu et al., 2022; Zelikman et al., 2022: Yuan et al., 2023; Lin et al., 2025), where multiple solutions are sampled, and an external signal selects the positive ones for model fine-tuning. Our approach, A phaVerus, builds upon these concepts but moves beyond the simple sample-and-file strategy. Our method additionally uses refinement and tree search to collect data, and the data is collected using multiple modules (e.g., outputs from Treefinement may be used to improve exploration). Additionally, AlphaVerus uses various forms of feedback-such as trinary, scalar, language, and verifier outputs- rather than just binary filtering. Conceptually, we can view A1 Al phaVerus as a meta-generation algorithm (i.e., a combination of parallel sampling, refinement, and tree search) that improves over time, rather than model trained on filtered outputs.
C. Methodology
Components Table 4 summarizes the components of our method at different stages, the feedback sources used, the models employed, and the data collected for bootstrapping.
15

---

AlphaVerus
Stage
Feedback
Model
Data Collected
Exploration
Verifier (errors)
LLM Parallel Sampling
Verified Translations
Treefinement
Verifier (value), Verifier (errors)
LLM Tree Search Refinement
Error Fix Triplets, Veri- fied Translations
Critique Module
Rules, Trivial Programs, Verifier (bi- nary), Comparison LLM
Regex, Prompted LLM, Exploit LLM
String Manipulation,
Exploit Pairs
Table 4: Different components used in iterative translation in AlphaVerus
Alorithm and Prompts We detail the complete algorithm for A Pha in Algorithm 1. We list the prompt used for Exploration stage in Listing C, prompt used for Treefinement stage in Listing C, prompl used for exploit and comparison model in Listing C and Listing C, and for inference in Listing C. Unless specified in the prompt, we use user, assistant pairs to simulate few-shot examples.
Verus Code Completion
Consider the following incomplete Verus code:
(program)
A.
The code contains the relevant spec functions and the preconditions (requires) and postconditions (ensures) for the main function. Your goal is to complete the function by adding the necessary procedure, along with proof statements (such as invaris antts, asserts, proof f blocks, etc.) to prove the program. Only output the new program and not the entire code. You are not allowed to create new functions; however, you can use any functions already defined they are within the scope.
Translation:
Exploration Prompt
Consider the following dafny code:
(program) *.*
Your goal is to convert the code to Verus code. Based the syntax gave you, convert the code to Verus. Note that you may need to make some datatype-related changes for it to work in Verus. Specifically, use the most appropriate ones from the syntax and code examples provided earlier. However, do not change invariants or specifications (ensures and requires clauses). Make sure to include the use statements, proper start of code using verus!, and empty fn main() as done the examples.
16

---

AlphaVerus
Translation Treefinement Prompt
SYSTEM:
Here are some examples of fixing verus code based on compiler error message:
Verus Error Fixing Example (i+1): ## Incorrect Code:
'Frust (incorrest_code)
## Error Message:
@error_message
".'
## Corrected Code after fixing the errors:
" 'rust
[corrected_code]
<Other Examples>
USER:
Given a Verus program with function signature, preconditions, postconditions, and code, fix the errors present in the code. Effectively return the complete verys program by fixing all proof statements or adjusting the code, such that the code compiles correctly. Do no modify function signatures requires, ensures or specs. Repeat: Do not ever modify those lines in ensures clause, requires clause, function signatures. Just edit the proof. **Only in case of overflow errors** you
make reasonable relaxations the size of the input variables. For instance, considering the input length of array to be any value less than 10 is not reasonable. Similarly for integer inputs, considering them to be small numbers is not reasonable. Choose bigger bounds for relaxation. You can also use spec functions, to estimate the max value, and impose a condition accordingly. For instance, if error is integer overflow while doing multiplication, you can add requires statement such as:
forall kk: int <= k < nums. len () ==> (0 <= # #[trigger] nums [k] nums [k] 132: :MAX)
[trigger]
However, absolutely no other changes to precondition and postcondition are permitted! Below is the program::
(program)
The program has following message:
...
(error_messsage
Solution Format:
[Thoughts on Error Message]
[Thoughts on Error Resclution]
[Thoughts Corner Cases, such Overflow etc.]
[Comples Code]
17

---

AlphaVerus
Translation: Exploit Model Prompt
You are a Verus exploit agent that finds trivial solutions for incomplete and inaccurate preconditions and postconditions. Your goal is complete the code by proposing trivial solutions that pass verification conditions. Here are some examples:
## Input Problem:
vstd: :pte::preldd::::;
verus!
S
// Define a function to calculate the nth power of 2
e
fn power (n: u32) -> (result: u32)
7
[Code Truncated]
// Define the function ComputePower to calculate n for given n fn compute_power (n: u32) -> (result: u32)
11
12
requires
13
n >= 0, n 10000, // arbitrary bound, verus can't handle infinite recursion
ensures
result == result,
## Trivial Solution:
1et mut result: u32 = 1;
let mut x: u32 0;
// invariant: <= x <= n, and result == Power (x)
while x!= n invariant
3
0 <= 8& <= n,
result result, // result Power (x),
x +- 1; result = result. wrdping (result)
10
11
result
// Main function, empty for now
16
En m)in() (}
18
// verus!
<0ther Examples>
Charactersitics of a trivial solution:
Usually 1-5 lines of code
2. Does not use any complex data structures
3. Usually returns constant values, that passes all test
Your task is to provide only the trivially completed code, given new program. Only output the new program and not the entire code.
18

---

AlphaVerus
Translation: Comparison Model Prompt
Consider the following function:
ruust
(ruat_code) ..
and ddafny (dafny_code)
Consider the preconditions and postconditions of the various functions in the two programs along with the spee functions present, that need to proven.
## Are the preconditions and postconditions from both the programs same? Note, since they from different programming languages, minor changes to be ignored. Minor changes include, adding extra preconditions to limit size of input in rust code, so to ensure overflows are not encountered, or reformulating implication statements. Such changes are not to be considered, and the answer should be yes, if they are same. Further, preconditions on size of input is reasonable, if there a possibility of overflow. For instance, for computing fibonacci numbers, using something like n;=47 reasonable, and answer should be yes. However, using n;=5 would be incorrect, and answer should be no. Remember, you have focus on ensures and requires clause of the main function as postconditions and preconditions respectively.
Follow the following format:
[What Preconditions and Postconditions of Program 1]
[What Preconditions and Postconditions of Program 2] [Step by Step Thoughts on comparison between conditions. Minor differences can be ignored]
Finally, answer in format to the question they are same: Therefore, both programs are same /not same, the final answer Yes/No:
Contamination Check Prompt
Consider the following set of program database:
''jjson
<in context exemplars>
...
## Task: Your task is to find the program that is same or very similar (250%) to this program:
(Program from dataset)
...
You should start the solution, by first thinking which programs would be closest and why. Then, you should output the json, containing the same keys as above: prog-num, num, program is possible that none of the programs closest, or even similar. In that case return empty json object.
D. Results
D.1. Reward Hacking
Next, we analyze the quality of translations without the critique phase. Figure 6 shows the effect of removing the critique models and continuing the self-improvement process on 100 examples from DafnyBench. Without the critique phase, the model is able to translate a large fraction of programs, but it is primarily because of learning to use ass ume (false false) which renders any implementation trivially verified. This is primarily used by human developers to debug their proofs. However, here A AlphaVerus figures out how to game the system by generating trivial proofs.
19

---

AlphaVerus
Translation Progress
40
Percentage Translated
Sets
30
mutable array
20
Basic NT Algos:
Fibo, Prime
10
Basic Syntax
0
0
2
3
4
Iteration
Figure 8: Translation Progress by Concept. The graph shows the incremental progress in translation capabilities as different programming concepts mastered.
There is also snowballing effect, where initially the model generates single program with assume (false), ) then learns to use it in all programs. This is evident from the leveling off of correct translations in the figure. While an obvious way is to disallow such statements (as done by our rule-based verifier), we see even more complicated cases of reward hacking, such as leaving small gaps in translated specifications or even generating degenerate translations, as illustrated Figure 7. We conclude that the critique phase is critical for filtering out misaligned programs and preventing reward hacking.
AlphaVerus enables strong proof annotation. Unlike our work which evaluates methods on the difficult task of generation that requires generating both code and proof, concurrent work on Verus evaluates on the task of proof annotation: generating proofs given correct code. This is simpler task since the code already known to be correct. We compare against SAFE (Chen et al., 2024) using their reported results with DSCoder-33B at Pass@ I 10, as their implementation is not publicly available. We also evaluate against Verus (Yang al., 2024) using their default configuration with 70B model.
As shown in Table 3, Al phhhVeruu outperforms SAFE by 17% and Auto by 10%. This is notable since AlphaVerus was not designed for the proof annotations task, while Auto Verus has correction prompts specifically engineered for the task. Their engineering also results reduced generalizability; for instance, Auto Verus cannot be evaluated on HumanEval as it doesn't 't support multi-function programs. Second, SAFE used over a month of GPT-4o invocations and thousands of programs, contrasting with our use of 562 Dafny programs and an openly available 70B model.
AlphaVerus learns new concepts over iterations. Next, our goal is to understand what the model learns over iterations that improves its ability to translate more complex programs and improve downstream performance. We manually inspect translations from each iteration of A phaVerus in attempt to qualitatively characterize the kinds of programs that the system gradually learns to translate. Figure 8 depicts the new concepts that we identified across iterations, starting with the ability to translate basic syntax, then basic numeric algorithms, and then the ability to work with mutable arrays and sets.
Cost-optimal model for inference. Next, compare the performance of different models increase the inference cost. We compare LLaMA-3 1-8B and LLaMA-3. 1..1-77 1-70B, using cost ratio of 1:8 based on current API pricing. That is, generating 8 outputs with LLaMA-3.C 1- has the same cost as generating output with LLaMA- 3.. 10BB. We show the accuracy each model as a function of cost in Figure 9. LLaMA-3. 1-8B achieves faster initial gains, reaching an accuracy 0.55 with 128 units of cost, while LLaMA-3,0 1- 1-70B requires about 4 times more cost to reach similar performance. other words, for cost-constrained scenarios, is preferable use the smaller model with more samples, but
20

---

AlphaVerus
0.56
0.54
0.52
Accuracy
0.50
0.48
0.46
Llama-3.1 8B
0.44
Llama-3.1 70B
0.42
0
200
400
600
800
1000
Cost-adjusted Generations
Figure 9: Performance scaling of LLaMA 3. 1B and LLaMA-3, 1....11000 1-70B with cost. LLaMA 3. 1.18BB shows better cost efficiency at lower compute budgets, while LLaMA-3.0 1-70B shows higher asymptotic performance.
the larger model has better asymptotic performance. Our findings echo those of Wu et al. (2024) and Snell et al. (2025).
D.2. Qualitative Analysis
Listing 2, Listing 3, and Listing show example Dafny-to- Verus translations from AlphaVerus, indicating that AlphaVerus is capable of complex translations. In particular, the translations involve multiple specifications, helper functions, and proof annotations, and individually reach up to 100 lines of Verus code. For formally verified code generation, Listing shows generated implementation and proofs for function that removes duplicates from a sorted vector while maintaining its sorted order. The model is given the function signature and the specification (the requi res and ensures clauses). AlphaVerus generates Rust implementation and proof annotations (c.g., invariant, proof, assert statements) that pass the verifier. Listing 5 shows a multi-function example, in which helper function is ssrrrmme fol- lowed by largest..rrim.ffete... completing nontrivial lemma.
function. addition function implementations, Listing 6 shows AlphaVerus
Listing 2, Listing 3, Listing show example tafny-to-Verus translation from AlphaVerus. Listing 5, Listing show example formally verified code generations from AlphaVerus.
E. Limitations and Future Work
Our results show promising performance and potential for scaling the methods proposed in this work. In particular, we achieved state-of-the-ant performance without any fine-tuning However, moving forward, exploring fine-tuning models and RI. algorithms guided by verifier feedback would be promising and important direction. Further, while our analysis shows the critique module being effective in preventing reward hacking, we believe investigating better methods for filtering misaligned specifications remains an important future direction. Finally, we believe that treefinement can be extended to other domains, and better search strategies can be developed for even better performance in this important task verified code generation.
21

---

AlphaVerus
Listing 2: Translation example.
1/---- Dainy program (input AlphaVerus)
function (n: nat): nat { if -- 0 then 0 else if (n-1) > then R(n-1) - else (n-1)) n
method calcR(n: (n: nat) returns (r: nat) ensures r == R(n)
0; var :=
11
while 1
12
decreases n-i
invariant 0 <= i <- (1)
invariant
16
:= i 1;
if > >i
:- 1;
20
clse
21
r := r i;
24
// ---- Verus program (all model-gencrated) use vstd::prelude:114
verus!
fn calc_r(n: usize) -> (r: usize) requires n 100000, // added relaxation to prevent overflow
n (a 1) / < usize::MAX, // added check to prevent overflox ensures
(n + 1) / 2,
13
let mut r: u128 0;
14
let mut i = 0;
while i n
invariant
&6 n,
18
true, decreases n 1,
22
i=it 1;
23
assert (i == n);
1et temp: u128
u128 (n u128 1)
26
assert (temp usize: :MAX as u128);
27
1et F: usize = temp as usi2e;
28
31
fn main () (
32
// verus!
22

---

AlphaVerus
Listing 3: Translation example.
------
Dainy progran (input AlphaVerus)
method SearchRecursive a: seqcint>, i: int, j: int, x: int returns (k: int)
decreases j-1;
requires 0 <= <= <= Jal;
ensures k != -1 ==> ==>a[k]] -1;
ensures i <
x;
ensures k == -1 ==> forall r < :: a 1= x7
ensures k == -1 ==> forall
<= r < 11 [[r] 1= xi
if
11
12
k = return;
if alj-1l x
16
:= j-1; return;
20
else
21
k == Searchhecursiveea, i, 3-1, x)
24
25
26
method SearchLeep( a: seq<int>, i: int, d: int, xt int returns (k: int)
requires 0 <= i <= <- lal;
ensures i k k 11
-1; -=> a[k] x;
29
ensures k !-
30
ensures k != -1 ==> forall r < :: alz] I= x;
ensures k == -1 ==> forall
<= < 1: a[r] 1= x;
if == ]
34
35
return -1;
var t :- ji
39
while t >
decreases ti invariant forall p <= alp] 1=
43
if a[t-1]
44
:= t-1; return;
47
48
clsc
52
53
k = 11;
23

---

AlphaVerus
Vesus program (all modsl-genezated) use vatdr:prelode:sgg
verua!
Searches element sequence using recursion.
in sesrch_ (a: aVec<i32>, i: usize, j: usize, x: 132) -> (k: 132)
requires
D <u 66 <= 3 <a a.lent),
j-1 Hic 100000 // added preconcition
132::MAX usize, // added precondition
12
ensures
14
k !m -1 an> alk as int] == X, foralliss not
air as int] x, =>> air int] X,
K -- -1 a>> forallies natl ca
decreases
j -
19
--
21
-1
e1se a(] - 1)
23
sasert (] 1 <= 132::MAX usizel;
24
18 j 132 as usize
(3
132
26
1 elsa
28
else :
30
search_ 1. x)
31
searches element sequence using a loop.
35
fn (s &Vank1322, 1: usise, usize, x: 132) >> (k: 132)
requires
0 1 <= 3 a.len(),
38
i-i L00000, // added preconéition
132::MAX usize, // added precondition
40
ensures
42
k -1 an> alk as int] =-
k 1 forall|2: natl c aad ale as intl !- X
k
forall
<e J alx int] 1=
45
if s=
47
zeLurn -27
49
lst mut t: usise 3;
50
while
invariant
<=
66 <= 1, ())
54
foraillp: natl <- s6 p < j --> alp as int] 1-
1MAX as usi2e, added invariant
56
decresses t,
57
aasert (t <= al))
61
if 1 <= :32: usize (
return It 132;
63
else
return -17
66
asserL
68
k-t- 1i
71
-1
73
main()
75
verus!
24

---

AlphaVerus
Listing 4: Translation example. We collapse some whitespace and lines with brackets due to space.
// Dašny program (input to Alphaveros) module OneSpec
datatype Variables Variables(valagg (value: int]
predicate Ivi Variablest { v.value -- 0
predicate incrementup tv: variables, vf: variablest && vf vevllu =n v.value
precicate Decrementop Variables, via Variablest 66 Vf vvauue =- v.value 1
datatype Step
12
IncrementBLepp) DecrementStep!]
14
predi (vx Variables, vi Variables, step: Step)
16
17
match step
(ncrementStep Tncrement 19, case (eczementStep(: => DecrementOply, yf
19
21
precicate Next (o: Varlables, vt Variables)
23
exiats NextStep vi, step)
24
26
module OnePretorol { dstatype Variables variables (value: int)
28
predicate InLt Iv: Variablest v.value
31
predicate incrementup (v: variables, vf: Variablest 6& vivvel mn v.value
33
predicate Decrementóp (v: Variables, vf: Variablest && yf vvllue e= v.value
35
datatype Step
Increment DecrementStep()
predicate (extStep(v: Veriables, via Varisbles, step: Step)
40
step
42
case InerementStep!! Tnorement 18, vS! case DecrementStep DecrementOp tv, v
43
45
predicate Next (v: Variables, vf: Variables) exista step 11 NextStep (v, vi, stop) )
47
50
module refinementProof
import Unespee import opened onePratacol
54
function rastroction (v: Variablas)
onespen.Wartables [
OneSpec. (v..vall
56
57
Lemma Inf (v: Variablas)
requires Tnít (9)
ensures UnaSpec.Inss Inst (Abstraccionnt))
61
lenma Let (v: Variables, v Variables)
zequires Next (v, v))
64
ensures Unašpec.Noxt libstraction (bstractionn(")))
66
vaz step il MextSteptv, vi, atep); step { case IncrementStep(! assest NeeSpec.Neext:eee (Abstraction (v)rr Onespess.Decremeettteee
68
71
case BacramentStep() => OneSpec. Spep ract Abstraction (v*), OneSpec. Tt
73
75
76
25

---

AlphaVerus
// ---- Verus program (a11 moda i-generated)
#tallow importss]
but Itinss:;
#talfow funused wannuse__mpprrre Importsi]
builtin_mecsossss
verea!
8 struct Variables
value: Lnt,
11 spec In (vi Variables) >> bool v.value -- 0
spec increment_og oply: Variables, Y_prime: Variablest v_prime value v.value
13
spec in decrement_.p Variables, Y_prime; Variablest +> bool v_prime. velue == v.value -
15 enum Step
Increment,
Decrement,
18
spec next_step(v: Varisbles, V_prime: Veriables, step: Step)
20
match step
Step: Increment increment_ope (V, v_prime), Siept:Decrement => decrement_op(W y_prime),
22
23
spec in next (v: Varisbles, Y_prime: Verisbles) -> bool 25
exists|step: Step) next_step(v, y_prime, step)
27
struct VeriablesProtoedl { value: int,
spec pnit_protocol (v: VacioblesProtocol)
v.value
32
spec in increment_op_ppooace VariablesProtorcl, v_prime: Variablesstooocoa)) -> bool v_prime. value -- v.value
33
fn jecrement_op_proooom (v: VartablesProtocol, v_primes tariablesPro:0001) -> bool v_prime. v.value
34
35
enum StepEratoco: Tncrement,
37
Decrement,
poxt_step_protoool (v: VariablesFrotocol V_prime: VariablesProtoool step: StepProtoooll -> bool match step
40
Stepirotocol: :increment e> increment_ooe pppprotcoopppoooooooooo y_prime),
42
StepFrotocol: :Decrement => petrement_oo__rottee (V, v_prime),
44
spec next next_protoool (#: YartahlesProtocal v_primes (artsblesProtoool) bool exletalstept SLepProtocoo] prceooeepp (v, y_prime, step)
46
47
spec abstraction voriahlesPretozol) Variables Variables | valuez v.value
49
proof In refinement_inite VarieblesProtooel) 51
init_protoccl (v), requires
54
56
init rastiooo
assert (L:ue);
proof In refinemert_nextt (v: YariableesProtooo,, v_prime: VarieblesProo.ooll
requires
61
next_protoccl (v, v_prime),
63
next (abstractiion abatrae: iectaciiooooin (v_pcime)),
65
assert (abetractioo vaauee rast (v). .value + abstraction (v_prime) value abstraction (V).
value 1);
assert (existslstep: Stepl next_step (abstraction abstraction (v_prime), step)
67
if iestrrattoo/___rimaet value == shatraction (v). +
[nxt__teppaaattrrrccc (V), (ystrattionvv_primn)) } else assert (aext_step htw.__stteebbstreeiiorr...
Enep::Tnerement]3 1
89
(notraction(y_prinne Szep: :Decrement)
71
72
assert (next (abstraction abstraction (
76
In main() (3
verus!
26

---

AlphaVerus
Listing 5: Multi-function example. First, we have AlphaVerus complete the helper function it prime given its specification and preceding code. Then we have AlphaVerus complete largest.prime.facto.
spec fn spec_prime___ sereeeeeeeerreeeeee (num: int, limit: int) bool
foralllj: int j limit ==> (# [(trigger] (num 3 jt)
spec in spec_ ppeceprine (num: int) bool spec_prime me_heleeeeeeeeee (num, num)
En is ppime (num: u32) -> (result: bool)
requires
11
num >= 2,
12
ensures
result <==> spec_prime (num as int), // ------- Model generation starts here let mut i 2;
16
1et mut result truez while < num
invariant
2 <= i <= num,
20
result <==> spec_ gepe__prme__eepeee helper (num as int, i as int),
21
22
if num $ i -- 0 result false;
25
+
26
result
29
30
fn Sargest_prime_faeee u32) -> (largest: u32)
31
requires
n >> 2,
34
1 largest n,
35
spec_ spec_prine (largest as int),
8 Largest == 0, foralllpl <=
spec_prime (p) & as int $ p <= largest, Model generation starts here
39
1et mut largest = 1;
40
let mut i = 2;
while i <
invariant
n, 1 <= largest <= i,
44
spec spec_ prime (largest as int),
i <- <- largest =-> spec_prime(1 int),
largest <= n,
48
n & largest -- 0,
49
foralllpl <= < as spec (p) & n as int $ == 0 ==> <= largest,
if is (i)
8
largest 1;
53
54
1 +=
assert largest & largest <= n); assert (apec_prime (largest as int));
57
58
assert (n 8 largest == 0);
assert (feralllpl 0 <= ss spec srime (p) & as int == ==> p <= largest);
largest
27

---

AlphaVerus
Listing 6: Lemma example. AlphaVerus completes the lemma Lemma.step.subrange
2
proof in Germa_step_subraate (ssusssgggrrggggsuusssrrg Seqechar>, string: Seq<char>)
requires
substring.Jen () 0,
string.len() substring.len())
6 ensures
(substring(0) -- string. (0, lebstring.len() as int) [0] & skubstring.skip
(1)
="= string.skip(1) subrange (0, substring. skip (1) len int))) ==> substring
string. (0, len () as int)), ,
decreases substring.len()
// -------- Medel generation starts here
let m cubstring.len()
15
1et n string.len();
14
assert (m > 0);
assert (m <- n);
1et string.subrange00,
int);
assert (h.len() ;);
18
assert (susstring. == h.)en());
if substring[0] -- h[0]
let k substring. skip (k) ();
21
assert (k)p (1)
22
let g = (tsiing..sippl...uurragg. (0, k as int)
23
essert(g.len) = k);
assert (k == substring.lend) - 1);
assert h.len 1);
26
if substring.skipt1 =" assert (substring(() -- h[0]);
27
if
28
assert (substtinnn)))) -- g. () 1); assert (substring.
assert (forallli: nat h.len ());
31
m ==> substring (1 as int] hli as
intl) by
assert (substring(0] == b101);
assert (substring, skip (1) ="= g);
assert (forallli: nat i
substring as int] g[i
as int - 11); assert (substring = h);
35
assert (substring --- h)
38
} else
39
assert (! (substring =" h));
else
assert (substring h);
43
44
else
assert (! (substring ="= h)
28

---

AlphaVerus
Algorithm Iterative Translation and Refinement
Input: Source programs Dae, initial data D y DE
exploit
Output: Verified target programs Degt Initialize t- 0.
while not converged do
(I) Candidate Generation Verification:
- 0: verified pairs;
Sunverifted < D: (x, y) pairs for refinement
foreach æ E Dac do
Generate candidate translations {uy} esppooro D!
Cz +- 0: verified pairs for this z; S2 +- 0: syntactically correct, unverified candidates for this
foreach do
1/ passes verification then
C. C- (xr,1;)) yj)}
else if y; is syntactically correct then
S₂ + S.U. {yr}
+ CUCr
if 2 = 0 then Sunverified <- Sunveritied {Zz v)ly E S
(II) Refinement via Treefinement Search:
foreach (x. Sunverified do
Initialize refinement tree with root node (y. e(y))
while max iterations not reached do
Select node (y/, e(v')) by REBASE scoring Generate refinements (1/3) Greime (V', ((y')())))))))))))) D 4
foreach 3/ do v/ passes verification then
C CU ((x,, 3/)]; record trajectory in C,
break (stop refining this candidate)
else Add (vh. e(y())) as child node to the refinement
(III) Filtering and Data Update:
Initialize D 1(++1) +- (+)) exploit
exploit
foreach (z., y) C do
critic rejects or f(x, y) = False or 2 Gesploii Syj (1)) Depteaa finds exploit then
Discard y
if exploit is found then
((++1)
explon +- D (i+1)
exploit {(,,, 2)}
Update D (++1)
22 UC
Update D (1+1)
<- (1)
yty U ((0.e()))))(
y-rg'
i i
return Dig + tvl (x. v) E D D2
29


Reviews:
[{"review_id": "BE4ycNtjav", "reviewer": "Reviewer_5hh1", "summary": "The paper introduces a novel (ensemble of) technique(s) for the translation and formal verification of programs using Verus, a library based on the Rust language. \nThe authors implement a 3 step process that utilizes an LLM to generate samples of a program translation and proof of formal verification, a tree based search to refine candidates that presents errors in the translation, and a final LLM critique step to test whether the specifications of the original program have been respected in the translation process and the formal proof has been conducted correctly. By iteratively applying this process, the successful translations are collected in a dataset to be used as in context examples for future iterations, leading to an incremental improvement in translation performance.\n\nThe novel contributions are in the combined usage of the tree based search (Treefinement) and the critique actor; the latter include very language specific specifications (string matching) but also more generalizable methods and looks promising to be used in other context as well.\n\n## update after rebuttal\nNothing really changed with the rebuttal. I believe the paper should be accepted.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful review and positive assessment of our work. We appreciate your recognition of AlphaVerus’s novelty, useful and interesting methodology, particularly the Treefinement and Critique components, while finding it a promising method for other contexts. We are happy to address your questions and suggestions below.\n\n---\n\n> Yes, the evaluation criteria of a successful translation and verification is sensible. The scope is limited to datasets with human labeled and verified translations to Verus, which are limited in size.\n\nThank you for the comments about sensible evaluation criteria. Regarding scope, we agree that current evaluation datasets (HumanEval-Verus, MBPP-verified, Sec 4) are limited. This is primarily because the research direction of formally verified code generation is still emerging, and verifying code is extremely difficult even for human experts. We would be excited if future work expands the scope of benchmarks. Aside from evaluation, we note that our pipeline makes limited assumptions about the underlying data, so we also see adapting AlphaVerus to different source domains as an exciting future direction.\n\n> It seems we just trust the critique in the final evaluation of translation. While the reward hacking analysis is nice, it's not clear yet whether we can fully trust the generated specs.\n\nThank you for raising this interesting point about the generated specifications. Indeed, ensuring that the generated specification aligns with the source intent is challenging, as specs lack formal guarantees relative to intent. In our case, we evaluated AlphaVerus on downstream tasks in which the specifications are human-written. This means that the generated specifications from the AlphaVerus pipeline were at least useful for improving verified code generation performance. \n\nIn addition, motivated by your feedback, we conducted a manual review on a random subset of 20 examples and found 95% to be correct and complete translations, suggesting that the AlphaVerus pipeline frequently produces reasonable specifications. However, fully trusting AI-generated specs is an open and challenging area for future work to explore. \n\n> The critique is also particularly useful to avoid the obvious reward hacking. However, it is unclear how scalable this last step is to other languages: it will require different human coded rules, and the peculiarity of other languages might also make reward hacking harder to identify.\n\nAlthough rules can vary by language, our critique stage includes components (comparison and exploit models) that make minimal assumptions about the target language. The rule-based component is also intentionally simple, involving basic pattern matching (e.g., checking for assume statements, trivial preconditions, and verifier bypass annotations). Most of these would carry over to other verification-oriented languages. Nonetheless, fully adapting AlphaVerus to other languages remains an interesting future direction.\n\n> I think the section on the critique could use a bit more exposition in the main paper, though the detail of the appendix is appreciated.\n\nThank you for highlighting this. We will incorporate a clearer and more detailed summary of the critique step directly into the main paper.\n\n---\n\nWe hope these responses address your points. We appreciate the encouraging feedback and believe these clarifications will strengthen the final paper. We are happy to discuss any further concerns.", "claims_and_evidence": "The claims seems to be well supported by the ablation studies showcased in the result and appendix sections. Treefinement is a win as it allows (in combination of exploration) to improve the results to best in class. The critique actor is also needed as showcased in figure 7. The idea is that without it the translations tend to degenerate in hacked solution rather than valid ones.", "methods_and_evaluation_criteria": "Yes, the evaluation criteria of a successful translation and verification is sensible. The scope is limited to datasets with human labeled and verified translations to Verus, which are limited in size.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "Experimental designs are sound and present a fair comparison of this methodology with baselines. As this is the first paper addressing translation and formal verification in Verus, benchmarks rely on the few-shots techniques using accessible and well performing LLMs, but not on other specialized prompting and verification strategies.\n\nIt seems we just trust the critique in the final evaluation of translation.  While the reward hacking analysis is nice, it's not clear yet whether we can fully trust the generated specs.", "relation_to_broader_scientific_literature": "This paper is relevant to work at the intersection of formal verification and LLMs.  Bootstrapping off one formal language to another is a common difficulty with data scarcity in the space. Beyond rust, this provides a promising method for using a lot of code.  I'd be curious if this works in math with isabelle proofs -> lean proofs or similar.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "The paper presents an interesting methodology to kick-start and augment datasets for translation and formal verification of programs. The feedback from the compiler during Treefinement looks particularly useful to generate sound proofs that pass the compiler test and thus are free of potential hallucinations, increasing the probability of the creation of valid of the code, especially in the early phases when an LLM could have trouble to generate valid proofs in the absence of data. The critique is also particularly useful to avoid the obvious reward hacking. However, it is unclear how scalable this last step is to other languages: it will require different human coded rules, and the peculiarity of other languages might also make reward hacking harder to identify.\n\nThe self-improvement mechanism using in-context examples is interesting and is a good way of getting self improvement without being able to fine tune a model.  That being said, its not clear if this approach is limited over methods that also improve the model weights as well.  It was interesting seeing the exemplars translate to other models.", "other_comments_or_suggestions": "I think the section on the critique could use a bit more exposition in the main paper, though the detail of the appendix is appreciated.", "questions_for_authors": "How can you evaluate the critique model in a general and scalable way.  It seems like the reward hacking analysis focuses on one particular hack, but I imagine there is no shortage of other hacks.\n\nCan you subsample proofs and manually verify to get numbers that can be trusted.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "iUe7ggKVJp", "reviewer": "Reviewer_3hti", "summary": "The paper introduces AlphaVerus, a framework for generating formally verified code using LLMs, with focus on the challenges of programming languages with limited training data. AlphaVerus works by translating verified code from programming languages with lots of examples, into the target programming language. First it generates candidate translations, then refines them using a tree search algorithm with code-verifier feedback, and finally filters misaligned specifications and programs. AlphaVerus can generate formally verified solutions for HumanEval-Verified and MBPP-verified.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful review of our paper. We're glad you found our approach reasonable and appreciated the evidence supporting AlphaVerus’s effectiveness including treefinement and critique phase to prevent reward hacking. We address your questions and suggestions below:\n\n---\n\n> One question I have is whether the comparison with SAFE and AutoVerus are valid, given they both differ in size and characteristics of datasets and the paper does not try SAFE or AutoVerus on the same datasets as AlphaVerus.\n\nWe do think the comparisons are valid, so let us make a few clarifications. First, the comparison in Table 4 uses the exact same benchmark dataset: MBPP-verified. SAFE++ and AutoVerus were specifically designed for the proof annotation task, so we used AlphaVerus on this task to give the baselines the strongest possible chance. Regarding SAFE++, the authors have not released their code, so we were limited to reporting their published numbers.\n\nFor the verified code generation tasks, we attempted to adapt the publicly available AutoVerus framework, but despite significant effort, could not achieve non-trivial performance. As we note in the paper, this is almost certainly due to their task-specific, hand-engineered prompts. \n\nFinally, we note that this research area is still emerging, and even SAFE++ and AutoVerus are fairly concurrent works, so we made our best effort to construct a fair comparison given their results and models. We would be happy to further clarify any other aspects of this evaluation. \n\n---\n\n> I wonder whether using Dafny as the source domain limits the applicability, since Dafny is not a mainstream language.\n\nOur goal in AlphaVerus is to perform formally verified code generation. Among automated program verification languages, Dafny is one of the most prominent in terms of code content and industrial use, including large-scale deployments [1]. \n\nFurther, our primary goal was demonstrating the *feasibility of the bootstrapping pipeline* (translation -> refinement -> critique -> self-improvement) in a realistic data-scarce setting for verified code. Dafny was chosen strategically because it *has* accumulated sufficient verified examples over time to serve as a viable source, unlike many target verification languages (like Verus). Crucially, our pipeline makes *minimal assumptions about the source language* (e.g., no source verifier needed). The core methodology – leveraging a higher-resource language, iterative refinement with verifier feedback, and critique – is applicable to other language pairs where a similar resource disparity exists.\n\n---\n\n> Appendix D states that \"critique [...] may not work in all cases, especially for more complex problems\". It would be beneficial to expand on this point...\n\nThis statement in the limitations (Appendix D) was included in the spirit of acknowledging *potential future challenges* as problem complexity scales significantly beyond current benchmarks. However, within our experiments on DafnyBench translation and HumanEval/MBPP-verified generation, we did not observe failure patterns where the critique allowed misaligned or trivially verified programs through. That said, identifying specific limitations of the critique component and improving it further would be an interesting direction for future work to explore. \n\n---\n\nWe hope these clarifications address your concerns. We value your feedback and believe these points strengthen our contribution. We look forward to addressing any additional questions or points you may have.\n\n## References:\n[1] Chakarov, Aleks, et al. Formally Verified Cloud-Scale Authorization. 2025, https://www.amazon.science/publications/formally-verified-cloud-scale-authorization.", "claims_and_evidence": "Claims supported by evidence:\n\n* The paper provides evidence that AlphaVerus improves the translation of programs from Dafny to Verus through more iterations. With experiments, it shows a steady increase in translation success rate.  \n\n* The authors show that Treefinement (their refinement approach) increases performance better than additional parallel sampling.\n\n* The critique phase is used to prevent reward hacking.\n\nOne question I have is whether the comparison with SAFE and AutoVerus are valid, given they both differ in size and characteristics of datasets and the paper does not try SAFE or AutoVerus on the same datasets as AlphaVerus.", "methods_and_evaluation_criteria": "Overall the approach seems reasonable. I wonder whether using Dafny as the source domain limits the applicability, since Dafny is not a mainstream language.", "theoretical_claims": "-", "experimental_designs_or_analyses": "Appendix D states that \"critique [...] may not work in all cases, especially for more complex problems\". It would be beneficial to expand on this point, if only to provide further characterization of the kinds of complex problems that lead to critique failure.", "relation_to_broader_scientific_literature": "-", "essential_references_not_discussed": "-", "other_strengths_and_weaknesses": "-", "other_comments_or_suggestions": "-", "questions_for_authors": "-", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "TfqEyuXnnx", "reviewer": "Reviewer_Bjqi", "summary": "The paper proposes a holistic approach for the LLM-based generation of verified code. First, the paper proposes an approach to address the scarcity of training/sample data in many real-world programming languages that could serve as code generation targets. To this end, the paper proposes an LLM-based technique that allows the translation of samples from \"data-rich\" languages to \"data-poor\" languages (e.g. from Dafny for which larger benchmark datasets exist to Rust). The paper evaluates the proposed translation pipeline (incl. ablation studies) and demonstrates the applicability of the resulting data set to verified code generation.\n\n## update after rebuttal\nI appreciate the authors' response which lifted all open questions on my side.\nI keep my score and am in favour of accepting the paper.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your very thoughtful review and your positive feedback on our work. We appreciate your recognition of AlphaVerus's potential and thorough understanding of our contributions. We address your points below:\n\n---\n\n> “However, I have to note that I am not convinced that the rule-based approach can filter out all cases where a specification becomes trivially verifiable. For example assume(false) could be rephrased into something like assume(0!=1)”\n\nThe critique modules components work in tandem to collectively filter out bad specifications, so we wouldn’t expect the rule-based filter to filter out all of them. Regarding the case you mentioned (assume(false)), we should clarify that we exclude all assume statements from final proofs, as they are only used for debugging. Therefore, variants like `assume(0 != 1)` will be filtered out. Further, our manual analysis (see response to Reviewer 1) found only 5% critique failiures. That said, we intentionally kept our rules here fairly simple, so expanding this part of the pipeline is interesting future work. \n\n---\n\n> “Other Comments Or Suggestions”\n\nWe thank the reviewer for the suggestions. We will update the algorithm accordingly. Further, to clarify, S from step 1 is only used if no correct solution is found. We will update the algorithm to make it clear.\n\n---\n\nWe also thank the reviewer for sharing additional references that demonstrate the widespread issue of data scarcity in verified code generation. We strongly agree with your perspective and greatly appreciate your acknowledgment that AlphaVerus addresses an important gap. We will appropriately incorporate the valuable citations you provided in our revised manuscript to further strengthen our motivation for AlphaVerus.\n\n---\n\nWe appreciate your valuable feedback and suggestions. We look forward to addressing any additional questions or points you may have.", "claims_and_evidence": "The claims of the paper are well supported by empirical evidence.", "methods_and_evaluation_criteria": "The paper uses appropriate methods for its objectives.\nWhile the \"Critique\" step of the translation pipeline does not provide any formal guarantees, the paper specifically discusses this limitation and the approach is nonetheless a significant step forward in correct translation.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "I checked the experimental results presented in the paper and appendix.\nIn my view, the paper does a good job at grounding its claims with experimental results.\nUnfortunately, there is no baseline to which a direct comparison would be possible.\nNonetheless, the authors put significant effort into comparing to related approaches where possible which is laudable.", "relation_to_broader_scientific_literature": "The paper indeed addresses an important problem:\nFor many programming languages that would be natural targets for LLM-based verified code generation or specification generation, there exists relatively little data that can be used for training, fine-tuning or prompting.\n\nLLM-based verification has also been attempted for other real world programming languages such as C with ACSL specifications [arxiv23,FASE24,CAV24] or Java with JML specifications [AI4MATH24,ISOLA24,GPCE24]. In many cases, the availability of benchmarks is an issue. Consequently, AlphaVerus is a very welcome contribution.\n\nSidenote: I do *not* expect you to cite all these publications, this is just meant to illustrate the wider landscape and emphasize that scarcity of data is a real problem.\n\n[arxiv23] https://arxiv.org/pdf/2311.07948  \n[FASE24] https://link.springer.com/chapter/10.1007/978-3-031-57259-3_13  \n[CAV24] https://link.springer.com/chapter/10.1007/978-3-031-65630-9_16  \n[AI4MATH24] https://openreview.net/forum?id=ZRTcPkNl7v  \n[ISOLA24] https://link.springer.com/chapter/10.1007/978-3-031-75387-9_15  \n[GPCE24] https://dl.acm.org/doi/10.1145/3689484.3690738", "essential_references_not_discussed": "no", "other_strengths_and_weaknesses": "I appreciate the effort the authors put into the filtering approach.  \nThe experimental results clearly show that this drastically increases the quality of translations, which is great!\n\nHowever, I have to note that I am not convinced that the rule-based approach can filter out all cases where a specification becomes trivially verifiable. For example `assume(false)` could be rephrased into something like `assume(0!=1)` (or even worse something depending on variables in the program but always evaluating to false).", "other_comments_or_suggestions": "Concerning Algorithm 1:\n- It is not clear from the algorithm that $D_{\\text{exploit}}$ is used in the if statement.  \n  If possible, it would be better to also adopt the $\\dots \\sim G_{\\text{exploit}}(\\dots)$ notation here\n- $D_{\\text{exploit}}^{(i+1)}$ seems to miss an initialization with $D_{\\text{exploit}}^{(i)}$\n- The algorithm looks like $S$ from step (I) is always used -- independently of whether a correct sample is found.  \n  This is confusing because on page 4 (at least superficially) it sounds like $S$ is only used if no correct sample was found.  \n  (\"If no candidates verify for source $x$, candidates that are syntactically correct proceed to refinement\")", "questions_for_authors": "none", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper proposes AlphaVerus, a method to augment the data for verified code generation by iteratively translating programs from high-resource to low-resource programming languages. After the exploration of translation, it subsequently does treefinement to search for program refinement using verifier feedback and filtering out misaligned programs to prevent reward hacking. Although the individual steps proposed in this work might not be novel (e.g., hi-res -> low-res translation, tree search, etc), the combination of use of language models and formal verification for generating verified code is interesting and novel. And more broadly, efforts in connecting the fields of programming language and machine learning research is always appreciated. The experiments are also well-constructed, as three LLMs and 2 programming datasets are used to show the effectiveness of the proposed method. And the specific evaluation used in this work (i.e., model must generate both the code and the proof annotations) is refreshing. Overall, I recommend an acceptance to the conference for this paper.
Decision: Accept (poster)