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.

When AI systems write computer code for critical applications like medical devices or autonomous vehicles, even tiny errors can have serious consequences. Current AI models, while impressive at generating code, cannot guarantee that their code will work correctly every time. We developed AlphaVerus, a system that teaches itself to write mathematically-proven, correct code. Like a student learning from both successes and mistakes, AlphaVerus tries different solutions, receives feedback from a mathematical verifier that checks if the code is correct, and in the process learns to generate more complicated code and fix its own mistakes. Our method achieves state-of-the-art performance in generating code that comes with a mathematical proof of correctness (known as formally verified code generation). AlphaVerus could enable AI to safely contribute to critical software systems where reliability is non-negotiable, from healthcare to aviation, while reducing the costly human effort currently required to verify code correctness.