Verifier-Grounded Agentic RL for Provably Correct Code

George Ma; Yuhao Zhang; Bing He; Zeren Shui; Ferhat Erata; Murali Krishna Ramanathan; Somayeh Sojoudi; Hao Zhou

cs.LGOct 13, 2026

Verifier-Grounded Agentic RL for Provably Correct Code

Authors: George Ma, Yuhao Zhang, Bing He, Zeren Shui, Ferhat Erata, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou

Organizations: UC Berkeley · AWS AI Labs

Abstract

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.

Figures & tables

Figure 1: The method. (a) In an episode, the policy takes one action per turn against a live verifier and revises based on its diagnostics. (b) Scoring a submission: the failed obligations and the hidden probes give the obligation ratio

\Omega

(Equation 1 ), while the integrity audit checks that the specification is intact and that no obligation was assumed instead of proved. (c) The ordering the score (Equation 2 ) induces: a verified candidate with an intact specification ranks highest, one that verifies only by weakening the specification ranks below an honest partial proof, and one that fails the proof check ranks below not submitting at all.

Panel of Figure 2 — Figure 2: An instance and the two tasks built from it. Each task removes a different part of a verified program and asks the model to restore it, leaving the specification given and unchanged.

	DafnyBench	SWE-Proof
Specification lines	16	117
Preconditions	1	4
Postconditions	2	8

Table 1: Median size of a specification in each benchmark.

Figure 3: The frozen proof specialist. (a) A policy is trained on annotation repair and then frozen. (b) In code generation, every submission is scored as the agent wrote it and again after the specialist rewrites its proof annotations, keeping the implementation. The episode takes the better score, and the specialist’s version is returned to the agent as feedback.

Figure 4: Held-out verified rate over training, per model size and task. Faint traces are per-step values and bold traces exponentially weighted moving averages; open and filled markers show the initial policy and the best checkpoint, with values above each panel. More curves are in Appendix F .

		Annotation repair			Code generation
Benchmark	Model	Init	RL	$\Delta$	Init	RL	$\Delta$
DafnyBench	Qwen3-1.7B	10.5	22.6	(+12.1)	13.9	27.0	(+13.1)
	Qwen3-4B	26.6	51.6	(+25.0)	43.4	52.5	( 0 +9.1)
	Qwen3-8B	38.7	53.2	(+14.5)	43.4	53.3	( 0 +9.9)
	Qwen3-14B	36.3	51.6	(+15.3)	41.8	50.0	( 0 +8.2)
	Qwen3.6-35B-A3B	67.4	76.7	( 0 +9.3)	66.1	93.5	(+27.4)

Table 2: Held-out verified rate (%) before and after verifier-grounded RL. Init is the initial policy and RL the best held-out checkpoint. The lower block evaluates the

35

B checkpoints trained on DafnyBench (Dafny, Verus) and SWE-Proof (Nagini) on benchmarks never used in training.

Figure 5: Code generation with and without the frozen proof specialist. Left and center: held-out verified rate at

35

B-A

3

B, with per-step values (faint) and moving averages (solid). Right: difference in best held-out rate at each DafnyBench scale.

Method	Annotation repair	Code generation
Untrained policy	67.4	66.1
Supervised fine-tuning	60.9	53.2
Binary outcome reward	75.2	71.0
Verifier-grounded reward	76.7	93.5

Table 3: Held-out verified rate (%) at

35

B on DafnyBench under different training signals. The binary outcome reward matches our run in every setting except the reward.

Appendix figures & tables18 assets

Supplementary material from the paper’s appendix.

Appendix

Task	Postcondition	Precondition	Safety	Invariant	Termination
Code generation	1.00	0.50	0.50	0.25	0.25
Annotation repair	0.50	0.25	0.25	1.00	0.25

Appendix

Table 5: Obligation category weights

w_{c}

used in Equation 1 .

	Qwen3-1.7B	Qwen3-4B	Qwen3-8B	Qwen3-14B	Qwen3.6-35B-A3B
Instances per step	8	8	8	8	16–32
Episodes per instance $G$	4	4	4	4	8
Learning rate	$1\times 10^{-6}$	$1\times 10^{-6}$	$1\times 10^{-6}$	$1\times 10^{-6}$	$2\times 10^{-6}$
KL coefficient	0.02	0.02	0.02	0.02	0.02
Update epochs per step	1	1	1	1	1–2
Max response tokens	4096	4096	4096	4096	8192–12288

Appendix

Table 6: Training hyperparameters.

G

is episodes sampled per instance. All runs are full-parameter; no adapters are used.

	Code generation			Annotation repair
Repository	Total	Train	Held-out	Total	Train	Held-out
Web framework (split)	231	184	0 47	111	88	23
Symbolic mathematics	0 75	0 75	00 0	0 43	43	0 0
Documentation generator	0 44	0 44	00 0	0 27	27	0 0
Plotting library	0 34	0 34	00 0	0 14	14	0 0
Machine learning toolkit	0 32	0 32	00 0	0 14	14	0 0

Appendix

Table 7: Per-repository composition of the SWE-Proof split. The largest repository is divided across both sides; every other repository lies entirely on one side.

Figure 7: DafnyBench over training, one column per model size. Rows one and two are annotation repair, held-out verified rate and mean training reward; rows three and four are code generation. Faint traces are per-step values, solid traces exponentially weighted moving averages.

Figure 8: SWE-Proof at

35

B: held-out verified rate (left column) and mean training reward (right column), annotation repair on top and code generation below. Annotation repair starts near zero, so essentially all of its final performance is acquired during training.

Figure 9: SWE-Proof held-out verified rate at every model size. Top row: annotation repair, which stays at or near zero below

35

B; note the compressed vertical scale on the first four panels. Bottom row: code generation with and without the frozen proof specialist, which are indistinguishable wherever the specialist itself is at the floor.

Figure 10: DafnyBench episode diagnostics over training at all five model sizes: turns per episode, submissions per episode, mean response length, the fraction of submissions failing the integrity audit, and policy entropy.

Figure 11: The same diagnostics on SWE-Proof at

35

B. Episodes are longer than on DafnyBench throughout, which is what a repository-scale instance with several routines to prove requires.

Run	Window	Submits/ep.	First-try	Retries	Revises	Recovers
DafnyBench codegen	early	2.28	52.8	87.6	96.8	38.2
DafnyBench codegen	late	1.98	66.9	99.4	98.9	53.7
DafnyBench repair	early	2.40	46.8	91.4	95.3	42.9
DafnyBench repair	late	2.72	42.9	97.9	98.6	47.2
SWE-Proof codegen	early	1.84	58.7	83.0	85.2	27.6
SWE-Proof codegen	late	1.24	82.5	100.0	89.7	89.3

Appendix

Table 8: Held-out episode behavior, early versus late in training. All columns but the first are percentages. First-try is the fraction of episodes whose first submission verifies. The last three condition on the first submission failing: whether the policy submits again, whether the resubmission changes the program, and whether the episode ends verified anyway.

Episodes	$n$	Direct (%)	Assisted (%)	Verify only with help	Verify only without
Held-out	1589	61.9	72.3	165	0
Training	16250	59.8	71.3	1874	0

Appendix

Table 9: Per-episode effect of the frozen proof specialist on DafnyBench code generation. Direct is the agent’s own candidate; Assisted is the score the reward used. The last two columns count episodes where assistance changed the verification outcome in each direction.

	Qwen3-1.7B	Qwen3-4B	Qwen3-8B	Qwen3-14B	Qwen3.6-35B-A3B
With specialist	27.0	52.5	53.3	50.0	93.5
Without specialist	27.9	51.6	48.4	48.4	88.7

Appendix

Table 10: Held-out verified rate (%) on DafnyBench code generation with and without the frozen proof specialist, at every model size.

Figure 12: DafnyBench code generation episode diagnostics with and without the frozen proof specialist. The two runs behave alike.

Figure 13: The same diagnostics on SWE-Proof code generation.

With frozen specialist			Without specialist
Step	Resolve	Verify	Step	Resolve	Verify
0	59.6	76.1	0	62.4	84.4
5	65.1	78.9	5	60.6	88.1
10	66.1	83.5	10	68.8	85.3
15	65.1	80.7	15	67.9	89.0
20	67.9	88.1	20	68.8	87.2

Appendix

Table 11: Every held-out pass of the two SWE-Proof patch generation runs, on the complete held-out split (

109

instances, one greedy sample each). Resolve is the fraction of issues whose patch passes the project’s withheld tests and verify the fraction of the same episodes whose Nagini program verifies with an intact specification.

		Held out		Training
Measure	Run	Slope	$p$	Slope	$p$
Resolve	With specialist	$+0.29$	$7.6\times 10^{-4}$	$+0.44$	$2.9\times 10^{-4}$
Resolve	Without specialist	$+0.05$	$6.7\times 10^{-1}$	$-0.15$	$3.2\times 10^{-1}$
Full verification	With specialist	$+0.30$	$5.5\times 10^{-3}$	$+0.59$	$1.1\times 10^{-5}$
Full verification	Without specialist	$+0.09$	$1.5\times 10^{-1}$	$+0.25$	$1.9\times 10^{-1}$

Appendix

Table 12: Fitted trends over the eight held-out passes and over the training steps of the same runs. Slope is in points of rate per training step, with the

p

-value of a two-sided test against zero slope.

Suite	Task	$n$	Init (%)	RL (%)	$z$	$p$
HumanEval-Dafny	repair	110	54.5	70.0	2.36	$1.8\times 10^{-2}$
HumanEval-Dafny	codegen	131	67.9	92.4	4.96	$7.1\times 10^{-7}$
HumanEval-Nagini	repair	0 77	23.1	36.4	1.81	$7.0\times 10^{-2}$
HumanEval-Nagini	codegen	0 90	40.7	54.4	1.86	$6.3\times 10^{-2}$
HumanEval-Verus	repair	0 84	0 9.5	13.1	0.73	$4.6\times 10^{-1}$
HumanEval-Verus	codegen	0 93	17.2	36.6	2.98	$2.9\times 10^{-3}$

Appendix

Table 13: Transfer significance, two-proportion

z

-tests on the instances where both the initial policy and the trained checkpoint were evaluated.

		No submission (%)		Unparseable turns (%)
Suite	Task	Init	RL	Init	RL
HumanEval-Dafny	repair	0 8.2	0.0	31.4	15.5
HumanEval-Dafny	codegen	0 8.4	0.0	18.6	13.2
HumanEval-Nagini	repair	0 5.1	0.0	34.6	25.3
HumanEval-Nagini	codegen	11.0	0.0	27.6	0 7.8
HumanEval-Verus	repair	13.1	0.0	56.3	32.8

Appendix

Table 14: Interaction quality on the transfer suites. No submission is the fraction of episodes that never produce a candidate; unparseable turns is the share of turns whose output contains no action the environment can execute.

		Multi-submit (%)		Submissions
Suite	Task	Init	RL	Init	RL
HumanEval-Dafny	repair	46.3	63.6	1.96	3.52
HumanEval-Dafny	codegen	41.8	32.8	2.73	1.64
HumanEval-Nagini	repair	93.8	60.7	6.00	3.11
HumanEval-Nagini	codegen	48.5	30.6	4.09	3.18
HumanEval-Verus	repair	83.3	63.6	2.33	3.64

Appendix

Table 15: Iteration among successful transfer episodes. Multi-submit is the fraction of successes that required more than one submission; submissions is the mean number among successes.

RL for Code Generation

Reinforcement learning for code generation trains models to write, repair, and optimize programs using execution-based and other task-specific feedback.

See all 147 papers

The Verification Horizon: No Silver Bullet for Coding Agent Rewards
Jun 24, 2026Binghai Wang, Chenlong Zhang, Dayiheng Liu +10Reward Modeling Reward Hacking
Qwen Team
Beyond the Verdict: Agentic Code Judging with Verifiable Feedback
Oct 13, 2026Zheye Deng, Sha Li, Changlong Yu +4LLM-as-a-Judge Code Generation Evaluation
HKUST · Amazon
Automating Formal Verification with Reinforcement Learning and Recursive Inference
May 29, 2026Max TanRL for Code Generation Inference-Time Search
Department of Electrical Engineering and Computer Science · Massachusetts Institute of Technology

Jun 24, 2026J/K move · Enter open · S save

The Verification Horizon: No Silver Bullet for Coding Agent Rewards

Binghai Wang, Chenlong Zhang, Dayiheng Liu, Jiajun Zhang+9

Qwen Team

Reward Modeling Reward Hacking AI Coding Agents LLM Agent Verification Reinforcement Learning with Verifiable Rewards Reward Design for RL

Open paper AskPDF arXiv

A classical intuition holds that verifying a solution is easier than producing one. For today's coding agents, this intuition is being inverted: as foundation models develop stronger reasoning capabilities and engineering harnesses grow more sophisticated, generating complex candidate solutions is no longer difficult -- reliably verifying them has become the harder problem. Every verifier we can build is only a proxy for human intent, never the intent itself. This makes verification subject to a twofold difficulty: first, intent is underspecified by nature, making it inherently hard to faithfully check whether it has been fulfilled; second, during model training, optimization widens the gap between proxy and intent -- manifesting as reward hacking or signal saturation. To address this, we characterize the quality of verification signals along three dimensions -- scalability, faithfulness, and robustness -- and argue that achieving all three simultaneously is the central challenge. We further study four reward constructions: a test verifier for general coding tasks, a rubric verifier for frontend tasks, the user as verifier for real-world agent tasks, and an automated agent verifier for long-horizon tasks. Across different task types and policy capability levels, we conduct in-depth analysis and experiments on the core challenges of reward design and how to more effectively leverage reward signals. Experiments show that targeted verification design can effectively suppress reward hacking, improve task completion quality, and achieve significant gains across multiple internal and public benchmarks. These experiences collectively point to a core observation: no fixed reward function can remain effective as policy capability continues to grow; and verification must co-evolve with the generator.

Abstract

RL for Code Generation

Explore similar work

The Verification Horizon: No Silver Bullet for Coding Agent Rewards

Beyond the Verdict: Agentic Code Judging with Verifiable Feedback

Automating Formal Verification with Reinforcement Learning and Recursive Inference