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

TL;DR

AlphaVerus introduces a self-improving framework that bootstraps formally verified code generation by translating programs from a resource-rich language (Dafny) into Verus and iteratively refining translations with verifier feedback. The core innovation lies in Treefinement, a verifier-guided tree-search refinement that, together with a critique module to prevent misaligned specifications, yields substantial gains in generating verified code without model fine-tuning. Empirically, AlphaVerus demonstrates increasing translation success, achieves non-trivial verified-code generation on HumanEval-Verus and MBPP benchmarks, and enables transfer of exemplars across models, all with open-model resources. The approach reduces reliance on human prompts and expensive initializations while providing a scalable pathway toward trustworthy AI-assisted programming. These results suggest formal verification can play a central role in building reliable, automated code-generation systems applicable to real-world software development.

Abstract

Automated code generation with large language models has gained significant traction, but there remains no guarantee on 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 a 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.

Figures (10)

• Figure 1: Overview of AlphaVerus, a self-improving framework for generating formally verified code. Each iteration consists of three key steps: (1) Exploration translates programs from a 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 to continuously improve performance without human intervention.
• Figure 2: Example of formally verified code generation and translation. The figure shows the three key components of formally verified code: specifications (left), implementation with proof annotations (right), and the verifier. The specifications define a mathematical predicate divides and use it to specify primality. The implementation includes both algorithmic code and proof annotations (highlighted in green), which together allow the verifier to prove that the implementation satisfies the specification (or provides error messages upon failure). Translation consists of translating a source input (e.g., a Dafny program) into specifications, an implementation, and proof annotations. AlphaVerus performs each task using a generator consisting of exploration followed by Treefinement, and a subsequent critique step for translation.
• Figure 3: Example of Verus verifier errors showing two issues: (1) an invariant violation at the end of a loop body and (2) a potential arithmetic overflow in an increment operation. Errors point to exact lines and the verification results indicate 2 successful and 1 failed verifications.
• Figure 4: Programs Translated over Iterations. The translation success rate shows consistent improvement over iterations.
• Figure 5: Treefinement vs. exploration (HumanEval). Treefinement leads to a jump in performance that cannot be obtained by additional parallel sampling (exploration).