ExVerus: Verus Proof Repair via Counterexample Reasoning

Jun Yang; Yuechun Sun; Yi Wu; Rodrigo Caridad; Yongwei Yuan; Jianan Yao; Shan Lu; Kexin Pei

cs.PLMar 26, 2026

ExVerus: Verus Proof Repair via Counterexample Reasoning

Authors: Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei

Organizations: The University of Chicago · Purdue University · The University of Toronto · Microsoft Research

Abstract

Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.

Figures & tables

Figure 1: Motivating example from VerusBench (Misc/findmax) showing advantages of source-level counterexample (the ExVerus counterexample generation on top right) v.s. Verus’s counterexample (Verus counterexample generation on button right).

		DeepSeek-V3.1	GPT-4o	Qwen3-Coder	o4-mini	Sonnet-4.5
VerusBench	Iterative Refinement	60.3	43.2	69.2	69.2	83.6
	AutoVerus	24.7	39.0	51.4	32.2	75.3
	ExVerus	71.9 ( $\uparrow$ 19.3%)	51.4 ( $\uparrow$ 19.0%)	71.9 ( $\uparrow$ 4.0%)	74.7 ( $\uparrow$ 7.9%)	88.4 ( $\uparrow$ 5.7%)
DafnyBench	Iterative Refinement	73.1	82.1	89.6	82.1	95.5
	AutoVerus	76.1	79.1	86.6	77.6	95.5
	ExVerus	88.1 ( $\uparrow$ 15.7%)	88.1 ( $\uparrow$ 7.3%)	95.5 ( $\uparrow$ 6.7%)	95.5 ( $\uparrow$ 16.4%)	95.5

Table 1: Repair success rate across different methods, models, and benchmarks. All rates are in percentages. Percentages in braces denote how ExVerus improves over the best baseline among Iterative Refinement and AutoVerus .

Category	Sub-strategy	All Obfuscated Programs
Category	Sub-strategy	DeepSeek-V3.1	GPT-4o	o4-mini	Qwen3-Coder	Sonnet-4.5
Layout	Identifier Renaming	81.5 / 25.9	50.0 / 31.5	74.1 / 25.9	81.5 / 38.9	87.0 / 66.7
Data	Dead Variables	81.7 / 27.9	40.8 / 20.4	79.2 / 17.1	76.2 / 30.4	90.4 / 62.9
Data	Instruction Substitution	79.9 / 24.7	42.9 / 24.0	78.6 / 18.8	73.4 / 31.8	90.3 / 66.2
Control Flow	Dead Code Insertion	73.9 / 30.4	26.1 / 8.7	87.0 / 8.7	65.2 / 21.7	78.3 / 56.5
	Opaque Predicates	86.4 / 31.8	27.3 / 18.2	86.4 / 13.6	77.3 / 31.8	90.9 / 77.3

Table 2: Performance on all obfuscated programs ( ExVerus / AutoVerus ). All results are success rates in percentages.

Model	Method	Tasks $\geq$ 5 invariants			Tasks < 5 invariants			Total
Model	Method	#Tokens	Cost	Time	#Tokens	Cost	Time	#Tokens	Cost	Time
DeepSeek-V3.1	AutoVerus	431.1/62.0	0.18	3463.0	411.4/35.3	0.15	2352.3	422.7/50.6	0.17	2989.1
DeepSeek-V3.1	ExVerus	111.2 / 14.6	0.05	702.2	68.7 / 15.0	0.04	746.5	93.8 / 14.8	0.04	720.3
GPT-4o	AutoVerus	118.2/62.8	0.92	305.5	57.5/23.9	0.38	137.6	92.3/46.2	0.69	233.9
GPT-4o	ExVerus	101.4 / 25.6	0.51	299.5	57.3 / 14.5	0.29	179.8	83.1 / 21.0	0.42	250.0

Table 3: Token consumption (input/output in 1k tokens), cost ($), and execution time (s) for ExVerus and AutoVerus , measured per task across DeepSeek-V3.1 and GPT-4o.

		DeepSeek-V3.1	GPT-4o	Qwen3-Coder	o4-mini	Sonnet-4.5
VerusBench	Iterative Refinement	60.3	43.2	69.2	69.2	83.6
	ExVerus no_mut	64.4	46.6	65.8	68.5	84.9
	ExVerus	71.9 ( $\uparrow$ 11.7%)	51.4 ( $\uparrow$ 10.3%)	71.9 ( $\uparrow$ 4.0%)	74.7 ( $\uparrow$ 7.9%)	88.4 ( $\uparrow$ 4.0%)
DafnyBench	Iterative Refinement	73.1	82.1	82.1	89.6	95.5
	ExVerus no_mut	88.1	89.6	92.5	85.1	95.5
	ExVerus	88.1	88.1	95.5 ( $\uparrow$ 3.2%)	95.5 ( $\uparrow$ 6.7%)	95.5

Table 4: Ablation study on mutation strategies. The results are success rates in percentage. Percentages in braces denote how ExVerus improves over the best baseline results among Iterative Refinement and AutoVerus .

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Repairing a wrong invariant that involves an invalid state by pinpointing and pruning it. Task Diffy/brs1 in VerusBench.

Figure 4: Identifying and removing a wrong invariant guided by counterexamples. Task CloverBench_two_sum_3 in ObfsBench.

Algorithm 1 ExVerus Pipeline 1: procedure ExVerus (

\mathcal{P},\Phi,\textit{model},\textit{MaxAttempts},\textsc{MaxZ3},k

) 2:

\Pi_{0}\leftarrow\textsc{InitProofGen}(\mathcal{P},\Phi,\textit{model})

(st,\ell)\leftarrow\textsc{Verify}(\mathcal{P},\Phi,\Pi_{0})

4: if

st=\textsc{Pass}

then 5: return {

\Pi_{0}

, status= Pass , phase=init_gen} 6: end if 7:

\Pi\leftarrow\Pi_{0}

8: for

t\leftarrow 1

to MaxAttempts do 9:

(st,\ell)\leftarrow\textsc{Verify}(\mathcal{P},\Phi,\Pi)

\triangleright

st,\ell

refer to status and verification log 10: if

st=\textsc{Pass}

then 11: return {

\Pi

, status= Pass , phase=cex_repair} 12: end if 13: if

st=\textsc{CompileError}

then 14:

\Pi\leftarrow\textsc{CompilationFixer}(\Pi,\ell,\textit{model})

15: continue 16: end if 17:

e_{t}\leftarrow\textsc{ExtractAndPrioritizeErr}(\ell)

18:

\Sigma_{t}\leftarrow\textsc{CexGen}(\Pi,e_{t},\textit{model},k,\textsc{MaxZ3})

19: if

\textsc{IsInvariantErr}(e_{t})\land\Sigma_{t}\neq\varnothing

then

\triangleright

Check if

e_{t}

is an invariant bug and

\Sigma_{t}

is not empty 20:

\Sigma_{t}^{val}\leftarrow\textsc{ValidateCex}(\mathcal{P},\Phi,\Pi,e_{t},\Sigma_{t})

21: else 22:

\Sigma_{t}^{val}\leftarrow\Sigma_{t}

23: end if 24:

\Pi^{\prime}\leftarrow\textsc{MutValRepair}(\Pi,e_{t},\Sigma_{t}^{val},\textit{model})

25: if

\Pi^{\prime}=\varnothing

then 26: continue 27: else 28:

\Pi\leftarrow\Pi^{\prime}

29: end if 30: end for 31:

(st,\ell)\leftarrow\textsc{Verify}(\mathcal{P},\Phi,\Pi)

32: if

st=\textsc{Pass}

then 33: return {

\Pi

, status= Pass , phase=cex_repair} 34: else 35: return {

\Pi

, status= Fail , phase=cex_repair} 36: end if 37: end procedure

Algorithm 2 Counterexample Generation (

\Sigma_{t}=\textsc{Solve}(\textit{z3py}_{t})

) 1: procedure CexGen (

\Pi_{t},e_{t},\textit{model},k,\textsc{MaxZ3}

) 2: for

i\leftarrow 1

to MaxZ3 do 3:

Q_{t}\leftarrow\textsc{MakeCexPrompt}(\Pi_{t},e_{t},k)

\triangleright

Q_{t}

is a query-generation prompt 4:

\textit{z3py}_{t}\leftarrow\textsc{QuerySyn}(Q_{t},\textit{model})

\triangleright

LLM translates

Q_{t}

to a Z3Py script 5:

(\textit{status},\textit{raw})\leftarrow\textsc{RunZ3}(\textit{z3py}_{t})

6: if

\textit{status}\neq\textsc{sat}

then 7:

Q_{t}\leftarrow\textsc{Feedback}(Q_{t},\textit{status})

8: continue 9: end if 10:

\textit{norm}\leftarrow\textsc{Normalize}(\textit{raw})

\triangleright

normalize format 11: if

\neg\textsc{SemanticValid}(\textit{norm},\Pi_{t})\ \textbf{or}\ |\textit{norm}|<k/2

then 12:

Q_{t}\leftarrow\textsc{Feedback}(Q_{t},\textsc{gatefail})

13: continue 14: end if 15: return

\textsc{MakeCEX}(\textit{norm},e_{t})

\triangleright

returns

\Sigma_{t}

16: end for 17: return

\varnothing

18: end procedure Algorithm 3 Mutation-based Counterexample-guided Repair 1: procedure MutValRepair (

\Pi_{t},e_{t},\Sigma_{t}^{val},\textit{model}

) 2:

(v_{t},r_{t})\leftarrow\textsc{ErrorTriage}(\Pi_{t},e_{t},\Sigma_{t}^{val},\textit{model})

M_{t}\leftarrow\textsc{MutatorSelect}(M_{all},v_{t})

\mathcal{C}_{t}\leftarrow\textsc{ApplyMutator}(M_{t},\Pi_{t},e_{t},\Sigma_{t}^{val},r_{t},\textit{model})

5: if

\mathcal{C}_{t}=\varnothing

then 6: return

\varnothing

7: end if 8:

\mathcal{C}_{t}\leftarrow\textsc{FilterCompilable}(\mathcal{C}_{t})

9: if

\textsc{AnyPass}(\mathcal{C}_{t})

then 10: return

\textsc{FirstPass}(\mathcal{C}_{t})

11: end if 12: return

\textsc{RankTop}(\mathcal{C}_{t},\Sigma_{t}^{val},e_{t})

13: end procedure

Appendix

Figure 5: Pseudo-code of ExVerus . Algorithm 1 illustrates the overall pipeline, Algorithm 2 illustrates counterexample generation, and Algorithm 3 illustrates mutation-based counterexample-guided repair.

Panel of Figure 6 — Figure 6: Venn charts per benchmark. AutoVerus ( ); ExVerus ( ).

Panel of Figure 7 — Figure 7: All-benchmarks Venn charts by difficulty (using GPT-4o). AutoVerus ( ); ExVerus ( ).

Benchmark	Technique	Invariants		Assertions		Proofs
Benchmark	Technique	low	high	w/o	w/	w/o	w/
VerusBench	AutoVerus	70.0	17.4	38.9	39.4	39.3	36.4
VerusBench	ExVerus	58.3	46.5	61.1	18.2	54.8	9.1
DafnyBench	AutoVerus	87.9	25.0	80.3	0.0	80.0	100.0
DafnyBench	ExVerus	93.1	75.0	90.9	0.0	90.8	100.0
HumanEval	AutoVerus	21.4	3.8	29.4	9.8	36.4	4.3

Appendix

Table 5: Success rate categorized by different bisections (number of invariants, w and wo assertions, w/ and wo proof functionsblocks) across different benchmarks. We use GPT-4o in this experiment.

Figure 8: A real example of error category given by the LLM-based error triage.

Explore similar work

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
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
Mar 18, 2026Zenan Li, Ziran Yang, Deyuan He +7Formal Verification Automated Theorem Proving
ETH Zürich · Princeton Language and Intelligence · Department of Computer Science, Princeton University +1
AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
Apr 24, 2026Pouya Pezeshkpour, Estevam HruschkaLLM Evaluation LLM Answer Verification
Megagon Labs

May 29, 2026J/K move · Enter open · S save

Automating Formal Verification with Reinforcement Learning and Recursive Inference

Max Tan

Department of Electrical Engineering and Computer Science · Massachusetts Institute of Technology

RL for Code Generation Inference-Time Search Automated Theorem Proving LLM-Based Program Synthesis Formal Verification Reinforcement Learning with Verifiable Rewards

Open paper AskPDF arXiv

Automated formal verification remains challenging for large language models because data for proof assistants and verification-aware languages is scarce, and correctness depends on satisfying precise machine-checkable specifications rather than producing plausible code. This thesis studies how verifier environments can improve LLM generation of verified programs and proofs through reinforcement learning from verifiable rewards (RLVR) and verifier-guided inference-time search. First, we train open-source models in Dafny with RLVR using Group Relative Policy Optimization (GRPO) and related variants, assembling generated candidates into complete programs and scoring them with compiler and verifier outcomes. Initial experiments on an APPS-derived Dafny dataset increased verified reward from 2.2% to 58.1%, but revealed specification hacking, where models exploit weak formal specifications instead of implementing the intended solutions. After filtering underspecified and vulnerable tasks, multi-turn RLVR on the refined benchmark improves the verified pass rate from 9.7% to 31.1%. Second, we develop a verifier-guided inference scaffold in Lean that treats proof generation as structured search over decomposed subgoals, verifier feedback, diagnostics, and repair. With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%. On the larger VERINA dataset, whole-task decomposition plus proof reviser solves 7 of 42 previously unsolved tasks. We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust

\texttt{curve25519-dalek}

verification project; preliminary results remain weak, indicating that stronger progress evaluation and task-specific tool-use policies are still needed.

Abstract

Explore similar work

Automating Formal Verification with Reinforcement Learning and Recursive Inference

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs