Verified Code Generation

Latest papers

15 papers3 papers in the last four weeks, with none the four weeks before. 0.0% of all new papers.

Verifier-Grounded Agentic RL for Provably Correct Code
Oct 13, 2026George Ma, Yuhao Zhang, Bing He +5RL for Code Generation Verified Code Generation
UC Berkeley · AWS AI Labs
Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification
Oct 5, 2026Yuxuan Jiang, Aditya Vempaty, Ashish JagmohanFormal Verification Recursive Self-Improvement
University of Maryland, Baltimore County · Emergence AI
Verification Trap: Understanding Test-Time Selection Failures under False Premises in Code Generation
Oct 4, 2026Feng He, Hejia Wang, Linghao Meng +2Execution-Guided Code Generation Code Generation Evaluation
University of Science and Technology of China, China · Beijing University of Posts and Telecommunications, China · National University of Singapore, Singapore +1
AI with Authority, from Application to Silicon
Aug 21, 2026Jason HickeyVerified Code Generation Formal Verification
Karyk
Vero: Can AI Agents Build Formally Verified Software Repositories?
Aug 13, 2026Zhe Ye, Hantao Lou, Yuechun Sun +8Code Generation Formal Verification
1UC Berkeley · University of Chicago · 3California Institute of Technology +3
P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation
Aug 10, 2026Zenan Li, Ziran Yang, Peiyang Song +2Code Generation Formal Verification
1Apodex · 2Princeton University · 3Caltech +1
Route-Align-Verify for Functional Correctness in Code Generation
Aug 4, 2026Erxue Zhou, Jingxiang Meng, Aofan LiuExecution-Guided Code Generation Code Generation
Software Engineering Institute, East China Normal University, Shanghai 200062, China · University of Chicago · Peking University
AxDafny: Agentic Verified Code Generation in Dafny
Jun 30, 2026Benjamin Breen, Austin Letson, Borja Requena Pozo +1Code Generation Formal Verification
Axiomatic AI, Boston, MA, USA.
Improving Small Language Models for Code Generation with Reinforcement Learning from Verification Feedback
May 28, 2026Egor Skopin, Evgeny KotelnikovRL for Code Generation Reward Shaping
Beyond pass@k: Redundancy-Aware RLVR for Multi-Sample Code Generation
May 27, 2026Le Bronnec Florian, Alexandre Verine, Rio Yokota +1RL for Code Generation Code Generation
RIKEN Center for Computational Science, Tokyo, Japan · École Normale Supérieure Paris, PSL University, Paris, France · LAMSADE, CNRS, Université Paris-Dauphine-PSL, Paris, France
Automating Formal Verification with Agent-Guided Tree Search
May 26, 2026Leo YaoCode Generation LLM-Based Program Synthesis
Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology
Viverra: Text-to-Code with Guarantees
May 14, 2026Haoze Wu, Rocky Klopfenstein, Keith Farkas +1Code Generation LLM-Based Program Synthesis
Amherst College · Broadcom
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
May 8, 2026Zichen Xie, Mrigank Pawagi, Yuxin Liu +5Code Generation Formal Verification
University of Virginia · 2Indian Institute of Science · 3Rice University +1
From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
Apr 24, 2026Md Erfan, Md Kamal Hossain Chowdhury, Ahmed Ryan +1LLM Prompting Code Generation
Department of Computer Science, The University of Alabama, Tuscaloosa, USA · Alabama Water Institute, The University of Alabama, Tuscaloosa, USA
WybeCoder: Verified Imperative Code Generation
Mar 31, 2026Fabian Gloeckle, Mantas Baksys, Darius Feher +5Verified Code Generation Formal Verification
FAIR, Meta · CERMICS, ENPC, Institut Polytechnique de Paris, CNRS · Computer Lab, University of Cambridge +3

Oct 13, 2026J/K move · Enter open · S save

Verifier-Grounded Agentic RL for Provably Correct Code

George Ma, Yuhao Zhang, Bing He, Zeren Shui+4

UC Berkeley · AWS AI Labs

RL for Code Generation Verified Code Generation Reinforcement Learning with Verifiable Rewards Code Generation Agentic RL Formal Verification

Open paper AskPDF arXiv

Reinforcement learning for code usually rewards passing tests, which a model can do while remaining wrong on the inputs the tests do not cover. A program verifier instead decides whether a program satisfies a formal specification for all inputs. Language models are almost always paired with verifiers at inference time only, and turning a verifier into a reward raises two difficulties. It reports only acceptance or rejection, which gives no gradient when every attempt fails, and a policy can cheat it, most simply by telling it to assume what the proof was supposed to establish. We build an agentic environment and reward that address both. The reward reads the verifier's diagnostics rather than its verdict, scoring a candidate by the weighted fraction of proof obligations it discharges, extended with hidden probes from a reference proof's annotations. An integrity audit outranks the verifier, rejecting any candidate that alters the specification or assumes what it was meant to prove. The model works as an agent against a live verifier over many turns, with a separately trained proof specialist as a frozen collaborator. Across Qwen3 models from 1.7B to 14B and a 35B Qwen3.6 mixture-of-experts model, held-out verification on code generation rises from 66.1% to 93.5% on DafnyBench and from 56.3% to 100% on SWE-Proof. This reward leads every other training signal we compare, including a binary pass-or-fail reward trained under otherwise identical settings, with the widest margin on code generation. When the agent must also deliver the repository patch, graded by each project's withheld tests, the fraction of held-out issues it resolves rises from 59.6% to 72.5%. Evaluated unchanged on three verification suites withheld from training, the checkpoints improve on all of them, including one whose language and verifier are absent from training.