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

arXiv: https://arxiv.org/abs/2412.06176 · HTML: https://mlsanity.com/paper/2412.06176/

## Key facts

- Cited by 35 papers in the map (data through 14 Oct 2026).
- Placed in Code and instruction data synthesis, one of 13 directions in Synthetic data and self-improvement for LLMs.
- Builds on 41 of its 55 references that are in the map.
- First posted on arXiv 9 Dec 2024.

## Placed in

- Synthetic data and self-improvement for LLMs / [Code and instruction data synthesis](https://mlsanity.com/synth/code-and-instruction-data-synthesis/)

## Builds on (most cited first, 30 of 41)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters](https://mlsanity.com/paper/2408.03314/) (2024)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing](https://mlsanity.com/paper/2305.11738/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [Scaling Relationship on Learning Mathematical Reasoning with Large Language Models](https://mlsanity.com/paper/2308.01825/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Check Your Facts and Try Again: Improving Large Language Models with External Knowledge and Automated Feedback](https://mlsanity.com/paper/2302.12813/) (2023)
- [The Effects of Reward Misspecification: Mapping and Mitigating Misaligned Models](https://mlsanity.com/paper/2201.03544/) (2022)
- [Generating Sequences by Learning to Self-Correct](https://mlsanity.com/paper/2211.00053/) (2022)
- [FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios](https://mlsanity.com/paper/2307.13528/) (2023)
- [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Sycophancy to Subterfuge: Investigating Reward-Tampering in Large Language Models](https://mlsanity.com/paper/2406.10162/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models](https://mlsanity.com/paper/2406.16838/) (2024)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Let's Sample Step by Step: Adaptive-Consistency for Efficient Reasoning and Coding with LLMs](https://mlsanity.com/paper/2305.11860/) (2023)
- [Self-Edit: Fault-Aware Code Editor for Code Generation](https://mlsanity.com/paper/2305.04087/) (2023)
- [RL4F: Generating Natural Language Feedback with Reinforcement Learning for Repairing Model Outputs](https://mlsanity.com/paper/2305.08844/) (2023)
- [Easy-to-Hard Generalization: Scalable Alignment Beyond Human Supervision](https://mlsanity.com/paper/2403.09472/) (2024)
- [Can ChatGPT replace StackOverflow? A Study on Robustness and Reliability of Large Language Model Code Generation](https://mlsanity.com/paper/2308.10335/) (2023)

## Built on by (most cited first, 30 of 35)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Efficient Test-Time Scaling via Self-Calibration](https://mlsanity.com/paper/2503.00031/) (2025)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Reward Hacking in the Era of Large Models: Mechanisms, Emergent Misalignment, Challenges](https://mlsanity.com/paper/2604.13602/) (2026)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System](https://mlsanity.com/paper/2510.09721/) (2025)
- [VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validation](https://mlsanity.com/paper/2504.15659/) (2025)
- [Propose, Solve, Verify: Self-Play Through Formal Verification](https://mlsanity.com/paper/2512.18160/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [Towards Repository-Level Program Verification with Large Language Models](https://mlsanity.com/paper/2509.25197/) (2025)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)
- [Robust Heuristic Algorithm Design with LLMs](https://mlsanity.com/paper/2510.08755/) (2025)
- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [Verifier-Guided Code Translation via Meta-Step Decoding](https://mlsanity.com/paper/2605.17626/) (2026)
- [Provably Complete Generalized Planning with LLMs](https://mlsanity.com/paper/2609.27105/) (2026)
- [LLM-Based Config Synthesis requires Disambiguation](https://mlsanity.com/paper/2507.12443/) (2025)
- [SoK: Understanding (New) Security Issues Across AI4Code Use Cases](https://mlsanity.com/paper/2512.18456/) (2025)
- [Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought](https://mlsanity.com/paper/2603.18334/) (2026)
- [ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning](https://mlsanity.com/paper/2604.27644/) (2026)
- [The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK](https://mlsanity.com/paper/2607.14340/) (2026)
- [An AI Approach to Verified Production Cryptographic Libraries](https://mlsanity.com/paper/2608.00965/) (2026)
- [Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change](https://mlsanity.com/paper/2609.16302/) (2026)
- [Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler](https://mlsanity.com/paper/2609.23954/) (2026)

## Abstract (arXiv)

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.