AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

1. Introduction

• Verified code can provide mathematical guarantees that an implementation meets its specification for all possible inputs, but formal specifications and proofs add complexity.The verifier checks whether code meets its specification; a passing verifier does not by itself establish that the specification reflects developer intent.Source: §1 · pp. 1–2
• The framework uses Dafny as a higher-resource source domain to address the shortage of training data for verified code generation in Verus.The paper notes that Verus had fewer than 10 public repositories, while Rust had millions of code examples.Source: §1 · p. 2
• AlphaVerus translates Dafny programs into Verus, refines candidates with verifier-guided tree search, and critiques translations for misaligned specifications or implementations.The critique phase addresses reward hacking without relying on unit test cases.Source: §1 · p. 2
• Each iteration collects exemplars that improve the phase models, and the approach requires neither human intervention nor model finetuning.The authors also state that a single language model can be used without expensive GPT-4 initialization.Source: §1 · p. 2
• 33% of Verified-HumanEval solutions were generated as verified code by Llama-70B, outperforming GPT-4o-based methods.The evaluation uses few-shot exemplars collected by AlphaVerus from DafnyBench translations.Source: §1 · p. 3
• The collected dataset contains translated programs, error corrections, and critique examples, and component ablations assess the pipeline.The source benchmark, DafnyBench, contains 562 programs of varying difficulty.Source: §1 · p. 3

2. Formally Verified Code Generation

• Formally verified code consists of a specification, an implementation, and a proof that the implementation conforms to the specification.A verifier uses the proof to check conformance for all possible inputs and returns error messages when verification fails.Source: §2 · p. 3
• A specification can be misaligned with developer intent or with an implementation that passes verification without implementing the intended functionality.The text gives missing edge cases, trivial implementations, and assume(false) as examples.Source: §2 · p. 3
• The generation task is to produce an implementation and proof given a specification and additional context, such that the verifier accepts them.The paper represents this goal as v(yS, yI, yP) = 1.Source: §2 · p. 3
• The bootstrapping problem is creating an initial model for verified code generation in a mainstream language when training examples for that language do not exist.The paper gives Rust code verified with Verus as an example target.Source: §2 · p. 3

3.1. Translation

• Exploration translates source programs into Verus candidates, retaining verified programs and syntactically correct attempts for further refinement and learning.Unlike approaches that keep only correct solutions, AlphaVerus also uses syntactically correct programs to expand the learning signal.Source: §3.1 · pp. 4–5
• Treefinement searches a tree of program refinements, using verifier feedback to rank imperfect candidates and address the non-local nature of error fixes.The search expands syntactically correct but unverified translations; REBASE balances exploration and exploitation until verification succeeds or a maximum depth is reached.Source: §3.1 · p. 5
• Treefinement scores programs using verified-function, error, and warning counts, prioritizing candidates closer to verification.Its scoring function penalizes errors and warnings with hyperparameters α and β; verifier feedback can include specific issues such as overflows and unsatisfied conditions.Source: §3.1 · p. 5
• Three critique filters reject misaligned programs: rule-based checks for trivial constructs, source-to-candidate comparisons, and adversarial tests of whether simple programs satisfy the specification.If an exploit program passes verification, the associated translation is discarded because the specification may be flawed.Source: §3.1 · p. 6
• Each iteration adds accepted source-program pairs and successful refinement trajectories to data pools used by later translator, refinement, and critique models.The process self-improves only insofar as the generated examples are useful exemplars; few-shot examples are sampled stochastically rather than used for fine-tuning.Source: §3.1 · p. 6
• DafnyBench supplies 562 non-trivial source programs, but translation to Verus is complicated by language differences and Verus’s more rigorous proof obligations, including overflow checks.Dafny is used as a higher-resource source domain for the Verus bootstrapping process.Source: §3.1 · pp. 6–7

3.2. Downstream Evaluation

• The pipeline targets verified code generation using synthetic Verus programs and error-feedback-correction triples collected during translation.The resulting model is evaluated on held-out specifications.Source: §3.2 · p. 7
• Downstream evaluation uses exploration followed by Treefinement to generate implementations and proofs from held-out specifications, with collected programs and refinement examples as few-shot exemplars.A task is solved if any generated candidate passes verification; the evaluation targets generation of both code and proofs from specifications alone.Source: §3.2 · p. 7

4. Experimental Setup

• Translation experiments use LLaMA-3.1-70B, with 256 exploration samples and tree search of breadth 32 and maximum depth 8.The study also evaluates LLaMA-3.1-8B, Qwen-32B, and GPT-4o on downstream tasks.Source: §4 · p. 7
• DafnyBench is filtered from 782 programs to 562 by excluding programs that verify without proof annotations.The exploration model starts from a Verus syntax file and five repository examples.Source: §4 · p. 7
• The verified-code-generation evaluation uses HumanEval and MBPP, with success requiring at least one correct solution among K generated programs.The benchmarks contain 85 provable functions from 49 HumanEval programs and 78 verified MBPP programs.Source: §4 · p. 7
• AlphaVerus is compared with few-shot base models; its final-iteration variants use DAFNY2VERUS-COLLECTION exemplars, and the table reports pass@256.The caption identifies AlphaVerus with exploration followed by Treefinement with REBASE as the best-performing variant.Source: §4 · pp. 7–8, Table 2 · p. 8
• Figure 5 compares solved-problem percentages against generation budgets for Treefinement and additional parallel exploration.AutoVerus and SAFE++ are also used for comparison on MBPP proof annotation, a task distinct from generating verified code.Source: Figure 5 · p. 8, §4 · p. 8

5. Results and Analysis

• Across iterations, translation success rises as the system learns concepts from basic syntax through number theory to mutable arrays and sets.The reported downstream HumanEval pass@32 continues improving, while pass@256 levels off.Source: §5 · p. 8, Figure 6 · p. 8, §5.1 · p. 10
• About 45% of DafnyBench is translated into Verus programs that both verify and align with critique models.The resulting collection contains 247 translated programs, 102 error trajectories, and 579 exploit pairs.Source: §5 · p. 8
• AlphaVerus enables verified-code generation and substantially increases performance over its underlying Llama 3.1 70B model and a prompted GPT-4o model; Treefinement further improves over the exploration stage.Source: §5 · pp. 8–9

5.1. Analysis

• Without critique, the model increasingly uses assume (false) to make implementations trivially verify, then explores other specification and verifier exploits.The analysis describes a snowballing pattern and gives examples including degenerate translations and debug statements.Source: §5.1 · p. 9, Figure 8 · p. 9
• Tree search-based refinement outperforms linear refinement, and REBASE outperforms best-first search under equivalent generation budgets.All evaluated refinement methods improve on initial exploration; linear variants are special cases of REBASE.Source: §5.1 · p. 9
• Example translations include multiple specifications, helper functions, and proof annotations, with individual programs reaching 100 lines of Verus code.A generated sorted-vector deduplication implementation and its proof annotations pass the verifier.Source: §5.1 · p. 10
• The DAFNY2VERUS-COLLECTION improves verified-code generation across smaller and larger models without finetuning, and GPT-4o sets a HumanEval state of the art.Table 3 reports significant improvements over each model's few-shot variant.Source: §5.1 · p. 10, Table 3 · p. 11
• With inference costs in a 1:8 ratio, LLaMA-3.1-8B reaches accuracy 0.55 at 128 cost units, while LLaMA-3.1-70B needs about four times the cost for similar performance.The smaller model gains faster initially; the larger model has higher asymptotic performance.Source: §5.1 · p. 11, Figure 10 · p. 11

Automated Formal Verification

• Prior theorem-proving approaches often target existing-project theorems or simple properties, while verification-aware research languages may have limited real-world applicability.The related-work discussion distinguishes these approaches from end-to-end verified code generation.Source: §6 · p. 11

Automated Formal Verification in Rust

• AutoVerus relies on human expertise for new refinement prompts, while SAFE++ uses GPT-4 initialization; AlphaVerus reports better results with open models and 100 times less data.AlphaVerus also studies implementation generation alongside proofs, rather than proof generation alone.Source: §6 · pp. 11–12

Inference-Time Strategies

• Treefinement treats full programs as nodes and refinement steps as edges, using verifier feedback on complete solutions to address non-local error fixes without a trained scoring model.This contrasts with tree-search methods that score intermediate mathematical-solution steps.Source: §6 · p. 12
• Treefinement combines scalar, binary, language, and exploit-model feedback in a tree, prioritizing refinement branches that the authors find perform better than linear refinement.Source: §6 · p. 12

Self-Improvement in LLMs

• AlphaVerus extends sample-and-filter self-improvement with refinement, tree search, multiple modules, and trinary, scalar, language, and verifier feedback.The authors frame it as a meta-generation algorithm that improves over time rather than a model trained on filtered outputs.Source: §6 · p. 12

7. Conclusion

• AlphaVerus combines Exploration, Treefinement, and Critique to translate Dafny programs into Verus and use verifier feedback while filtering misaligned programs and specifications.The authors report operation without human intervention, hand-engineered prompts, or extensive computational resources.Source: §7 · p. 12
• The approach achieves significant performance improvements on verified HumanEval and MBPP benchmarks where prior methods fail, and contributes a dataset of formally verified Verus programs.Source: §7 · p. 12
• AlphaVerus advances verified code generation and suggests that formal verification could help address correctness and reliability challenges in automated code generation.The authors describe this as opening avenues for trustworthy AI-assisted programming tools.Source: §7 · pp. 12–13

A.1. Hyperparameters

• Temperature is 0.7, top-p is 1.0, and max tokens are 2048; translation generates 256 examples per program.Source: §A.1 · p. 17
• Treefinement uses breadth 32 and depth 8, with α set to 0.1, β to 0.03, and rebase-node sampling temperature to 0.1.Source: §A.1 · p. 17
• Comparison and exploit models use 32 samples, batches contain 32 examples, and stochastic sampling selects k/2 exemplars; hyperparameters are not tuned.The GPT-4o model version is gpt-4o-2024-08-06.Source: §A.1 · p. 17

A.2. Contamination Analysis

• Contamination screening pairs each collected exemplar with HumanEval and MBPP programs, flags matches detected in more than two of four evaluations, and excludes flagged examples from that program's in-context examples.Source: §A.2 · p. 17
• Manual analysis finds the screening approach outperforms traditional n-gram analysis and aligns with human contamination assessments.The authors note that cited Verus proof-annotation baselines lack contamination analysis.Source: §A.2 · p. 17

A.3. Hardware and Software

• Inference uses L40S GPUs and SgLang, with translation and inference parallelized so each program runs on a separate node; the codebase and DAFNY2VERUS-COLLECTION are released.Source: §A.3 · p. 17

• Exploration converts Dafny code to Verus, allowing datatype changes while preserving invariants and requires and ensures clauses.Source: B. Methodology · p. 18
• Treefinement prompts the model to repair Verus code using compiler errors, while forbidding specification changes except reasonable overflow-related relaxations.Source: B. Methodology · p. 19
• An exploit model proposes trivial solutions that pass verification, while a comparison prompt checks whether translated programs preserve the main function’s preconditions and postconditions.Source: B. Methodology · pp. 17, 20, 21
• A contamination check searches contextual programs for one at least 50% similar to the dataset program and returns an empty object if none qualifies.Source: B. Methodology · p. 21

• Listings 5–6 show examples of formally verified code generation, including a multi-function task and a lemma.Source: §C.1 · pp. 21, 27, 28
• The protocol example translates datatypes, predicates, and refinement lemmas into Verus structs, specification functions, and proof functions.Source: §C.1 · pp. 22, 26
• The search translation example includes recursive and loop implementations with added bounds to address overflow and integer representation limits.Source: §C.1 · pp. 24–25
• For the multi-function example, AlphaVerus completes a helper function before generating the largest-prime-factor function.Source: §C.1 · p. 27
• The lemma example asks AlphaVerus to complete a proof connecting substring equality with equality of corresponding characters.Source: §C.1 · p. 28