SEVerA: Verified Synthesis of Self-Evolving Agents

Debangshu Banerjee; Changming Xu; Eugene Ie; Ming Zhang; Daiyi Peng; Chu-Cheng Lin; Tarun Suresh; Gagandeep Singh

cs.LGMar 26, 2026

SEVerA: Verified Synthesis of Self-Evolving Agents

Authors: Debangshu Banerjee, Changming Xu, Eugene Ie, Ming Zhang, Daiyi Peng, Chu-Cheng Lin, Tarun Suresh, Gagandeep Singh

Organizations: University of Illinois Urbana-Champaign, USA · Google, USA

Abstract

Recent advances have shown the effectiveness of self-evolving LLM agents on tasks such as program repair and scientific discovery. In this paradigm, a planner LLM synthesizes an agent program that invokes parametric models, including LLMs, which are then tuned per task to improve performance. However, existing self-evolving agent frameworks provide no formal guarantees of safety or correctness. Because such programs are often executed autonomously on unseen inputs, this lack of guarantees raises reliability and security concerns. We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility. We introduce Formally Guarded Generative Models (FGGM), which allow the planner LLM to specify a formal output contract for each generative model call using first-order logic. Each FGGM call wraps the underlying model in a rejection sampler with a verified fallback, ensuring every returned output satisfies the contract for any input and parameter setting. Building on FGGM, we present SEVerA (Self-Evolving Verified Agents), a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning; and Learning applies scalable gradient-based optimization, including GRPO-style fine-tuning, to improve the soft objective while preserving correctness. We evaluate SEVerA on Dafny program verification, symbolic math synthesis, and policy-compliant agentic tool use ( $τ^2$ -bench). Across tasks, SEVerA achieves zero constraint violations while improving performance over unconstrained and SOTA baselines, showing that formal behavioral constraints not only guarantee correctness but also steer synthesis toward higher-quality agents.

Figures & tables

Figure 1. Overview of SEVerA, which operates in four steps. (1) Ideation: given the task information, library functions $\mathcal{F}_{c}$ , and parametric generative models (GMs) $\mathcal{F}_{p}$ , the planner LLM proposes task-specific FGGMs, each binding a GM call to local contracts $(\Phi_{l},\Psi_{l})$ , a prompting program $f_{p}$ , a verified fallback $f_{d}$ , and expands the library components. Steps (2) and (3) form component-based synthesis : (2) Search: the planner emits a parametric agentic program over the expanded library, including parametric FGGMs; (3) Verify: the verifier checks all FGGM definitions and the program against $(\Phi,\Psi)$ , accepting valid programs and otherwise returning an error to the planner. (4) Learn: the GM parameters within each FGGM are tuned to improve conformance with the local contracts and to increase reward $\mathsf{R}{}$ over $\mathrm{D}$ . SEVerA maintains a pool of verified fine-tuned agents, reuses their traces to seed new candidates via step (1), and returns the highest- $\mathsf{R}{}$ agent.

Panel of Figure 2 — Figure 2. Guarded GM with a stateful rejection sampler (1) and fallback (2).

Panel of Figure 3 — Figure 3. Two example candidate parametric programs generated for symbolic regression.

Figure 4

Figure 5

Dataset	Total	Train
HumanEvalDafny	135	30
DafnyBench	760	50
$\tau^{2}$ -bench Retail	114	15
$\tau^{2}$ -bench Airline	50	10
GSM-Symbolic	100	50
Symbolic Regression	1000	600

Table 1. Dataset sizes and train/test splits.

Dataset	Method	Ver. & NoDiff (%) $\uparrow$		Ver. (%) $\uparrow$		Vio. (%) $\downarrow$		Time (s)
HumanEvalDafny	LLM (Claude Sonnet 4.5)	73.7		76.8		8.1		9.8
	DafnyBench baseline	86.9		87.9		4.0		16.1
	SEVerA (w/o constraints)	84.8		88.9		5.1		15.7
	SEVerA	97.0	(+10.1)	97.0	(+9.1)	0.0	(-4.0)	18.2
DafnyBench	LLM (Claude Sonnet 4.5)	68.7		71.1		10.3		10.3
	DafnyBench baseline	81.6		84.0		8.2		20.1

Table 2. Dafny program verification results on HumanEvalDafny and DafnyBench. Verif. & NoDiff counts a program as correct only if it both verifies and passes the AST-based diff check against the original; Verif. counts verification alone.

Domain	Method	Pass Rate (%) $\uparrow$		Violation (%) $\downarrow$		Time (s)
Retail	LLM (Qwen3-8B)	11.3		76.3		146.6
	Agent-C (Qwen3-8B)	42.2		0.0		234.7
	SEVerA (w/o constraints)	49.4		10.3		238.3
	SEVerA	53.6	(+11.4)	0.0	(0.0)	212.4
Airline	LLM (Qwen3-8B)	13.2		68.4		184.8
	Agent-C (Qwen3-8B)	39.4		0.0		272.6

Table 3.

\tau^{2}

-bench results with Qwen3-8B on the retail and airline domains. Higher pass rate is better; lower violation rate is better.

Method	Accuracy (%) $\uparrow$		Violation (%) $\downarrow$		Time (s)
LLM (Qwen3-8B)	38.3		10.6		10.9
CRANE ( Banerjee et al., 2025 )	44.7		2.1		18.4
SEVerA (no parameter tuning)	53.2	(+8.5)	0.0	(-2.1)	12.8
SEVerA (with parameter tuning)	66.0	(+21.3)	0.0	(-2.1)	11.7

Table 4. GSM-Symbolic results with Qwen3-8B. Higher accuracy is better; lower violation rate is better. Parenthetical gains are relative to CRANE.

Table 10

Configuration	Accuracy (%) $\uparrow$		Violation (%) $\downarrow$
LLM (Qwen3-8B)	38.3		10.6
SEVerA (no parameter tuning)	53.2	(+14.9)	0.0	(-10.6)
SEVerA (local only parameter tuning)	55.3	(+17.0)	0.0	(-10.6)
SEVerA (global only parameter tuning)	61.7	(+23.4)	0.0	(-10.6)
SEVerA (full)	66.0	(+27.7)	0.0	(-10.6)

Table 7. Constraint decomposition ablation on GSM-Symbolic (Qwen3-8B). Local = FGGM contracts only; Global = behavioral specification only; Full = both. Parenthetical gains are relative to the vanilla LLM.

Benchmark	Trig. $\downarrow$	FB Acc.	Gain	Gain ∗
HumanEvalDafny	5.1	5.1	+10.1	+8.1
DafnyBench	7.9	29.3	+7.5	+5.9
$\tau^{2}$ -Retail	15.6	5.2	+11.4	+10.6
$\tau^{2}$ -Airline	21.6	5.4	+13.2	+9.7
GSM-Symbolic	2.1	0.0	+21.3	+21.3

Table 8. Fallback trigger rate and impact. Trig. : fallback produces final output; FB Acc. : fallback-only baseline; Gain ∗ : gain excluding fallback instances.

Benchmark	Sampler	Trig. $\downarrow$	Perf. $\uparrow$
HumanEvalDafny	Stateless	9.1	88.8
HumanEvalDafny	Stateful	5.1	97.0

Table 9. Stateful vs. stateless rejection sampling. Trig. : fallback trigger rate; Perf. : task performance.

Appendix figures & tables16 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 4 — Figure 4. FGGM definition for ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ . The prompting function builds context-specific guidance by checking for lemmas, generics, sets, and multisets in the base program, and appends the auto-synthesized rejection feedback $err$ (the failing atomic formulas of $\Psi_{l}$ ) to make the rejection sampler stateful. The output processor $f_{post}$ extracts the annotated program from the fenced code block in the raw model response. The fallback returns the original program, satisfying $\Psi_{l}$ by the reflexivity axiom. Fallback trigger rate: 5.1% on HumanEvalDafny (Table 8 ).

Panel of Figure 5 — Figure 5. FGGM definition for ${\color[rgb]{0.293,0,0.5117}diffErrorFGGM}$ . Invoked when the previous iteration’s output failed the diff checker. The prompt includes the diff error and previous attempt, instructing the model to preserve the base program logic, and appends the auto-synthesized rejection feedback $err$ to prevent repeated mistakes. The output processor $f_{post}$ extracts the corrected program from the raw model response. Fallback trigger rate: 5.1% on HumanEvalDafny (Table 8 ).

Panel of Figure 6 — Figure 6. FGGM definition for ${\color[rgb]{0.293,0,0.5117}verifierErrorFGGM}$ . Invoked when the previous iteration passed the diff checker but failed verification. The prompting function analyzes the verification error to provide targeted guidance (timeout, lemma, invariant, or type issues) and appends the auto-synthesized rejection feedback $err$ , enabling the stateful rejection sampler to avoid repeated failures. The output processor $f_{post}$ extracts the corrected program from the raw model response. Fallback trigger rate: 5.1% on HumanEvalDafny (Table 8 ).

Panel of Figure 7 — Figure 7. Verified agent program for Dafny annotation synthesis. On the first iteration, ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ (Fig. 4 ) generates an initial annotation. On subsequent iterations, the agent dispatches to ${\color[rgb]{0.293,0,0.5117}diffErrorFGGM}$ (Fig. 5 ) or ${\color[rgb]{0.293,0,0.5117}verifierErrorFGGM}$ (Fig. 6 ) depending on the previous error type. Each FGGM guarantees ${\color[rgb]{0.293,0,0.5117}noDiff}(base\_program,y)$ via a rejection sampler with $K=5$ and stateful ${\color[rgb]{0.293,0,0.5117}Err_{\Psi_{l}}}$ feedback, maintaining the loop invariant. The fallback fires on only 5.1% of instances (HumanEvalDafny) and 7.9% (DafnyBench), confirming that the ${\color[rgb]{0.293,0,0.5117}Err_{\Psi_{l}}}$ -guided sampler produces conforming outputs in most cases. Upon exhausting all attempts, the agent returns $best$ , which satisfies the postcondition by the loop invariant.

Panel of Figure 8 — Figure 8. FGGM definition for ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ (GSM-Symbolic). The prompting function provides rules and examples for generating valid math expressions and appends the auto-synthesized rejection feedback $err$ , enabling the rejection sampler to avoid repeating syntactic mistakes. The output processor $f_{post}$ extracts the expression wrapped in << >> from the raw model response. The fallback returns “0”, a trivially valid expression. Fallback trigger rate: 2.1% (Table 8 ).

Panel of Figure 9 — Figure 9. FGGM definition for ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM1}$ (GSM-Symbolic). Invoked on the first parse-error recovery attempt. The prompt provides the failed expression and error details, and appends the auto-synthesized rejection feedback $err$ that accumulates parse errors across samples. The output processor $f_{post}$ extracts the corrected expression from the raw model response.

Panel of Figure 10 — Figure 10. FGGM definition for ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM2}$ (GSM-Symbolic). Invoked on the second parse-error recovery attempt with a checklist-style prompt that appends the auto-synthesized rejection feedback $err$ . The output processor $f_{post}$ extracts the corrected expression from the raw model response.

Panel of Figure 11 — Figure 11. FGGM definition for ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM3}$ (GSM-Symbolic). A minimal last-resort prompt used on the third and subsequent parse-error attempts, appending the auto-synthesized rejection feedback $err$ . The output processor $f_{post}$ extracts the corrected expression from the raw model response.

Panel of Figure 12 — Figure 12. Verified agent program for GSM-Symbolic. The agent first generates an expression via ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ , then enters a repair loop dispatching to ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM1}$ / ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM2}$ / ${\color[rgb]{0.293,0,0.5117}parseErrorFGGM3}$ based on the attempt number. Each FGGM guarantees ${\color[rgb]{0.293,0,0.5117}gsmParser}(\cdot)$ via a rejection sampler with $K=5$ and stateful ${\color[rgb]{0.293,0,0.5117}Err_{\Psi_{l}}}$ feedback. The fallback fires on only 2.1% of instances (Table 8 ).

Panel of Figure 13 — Figure 13. FGGM definition for ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ ( $\tau^{2}$ -bench). The FGGM emits an array of tool-call actions ( $arr\langle{\color[rgb]{0,0,1}str}\rangle$ ), and $\Psi_{l}$ uses the sequence-level checker ${\color[rgb]{0.293,0,0.5117}agentCCheckList}$ that verifies every action complies with the Agent-C policy given the trace extended by the preceding actions. The prompting function provides domain-specific instructions and appends the auto-synthesized rejection feedback $err$ , enabling the rejection sampler to avoid repeating non-compliant action arrays. The output processor $f_{post}$ parses the ordered array of tool calls from the raw model response, and the fallback returns a singleton array that transfers to a human agent. Fallback trigger rate: 15.6% retail, 21.6% airline (Table 8 ).

Panel of Figure 14 — Figure 14. FGGM definition for ${\color[rgb]{0.293,0,0.5117}duplicateFGGM}$ ( $\tau^{2}$ -bench). Invoked when the generated action array duplicates the previous one. The prompt instructs the model to try a different approach and appends the auto-synthesized rejection feedback $err$ to prevent repeated non-compliant action arrays. The FGGM returns an array of tool-call actions ( $arr\langle{\color[rgb]{0,0,1}str}\rangle$ ); $f_{post}$ parses this array from the raw model response.

Panel of Figure 15 — Figure 15. FGGM definition for ${\color[rgb]{0.293,0,0.5117}agentCErrorFGGM}$ ( $\tau^{2}$ -bench). Invoked when the generated action array fails the Agent-C policy check. The prompting function analyzes the offending tool name to provide targeted recovery guidance and appends the auto-synthesized rejection feedback $err$ , enabling the stateful rejection sampler to progressively narrow toward compliant action arrays. The FGGM returns an array of tool-call actions ( $arr\langle{\color[rgb]{0,0,1}str}\rangle$ ); $f_{post}$ parses this array from the raw model response.

Panel of Figure 16 — Figure 16. Verified agent program for $\tau^{2}$ -bench. The agent generates an array of tool-call actions via ${\color[rgb]{0.293,0,0.5117}initialFGGM}$ , then enters a loop that detects duplicate action arrays (dispatching to ${\color[rgb]{0.293,0,0.5117}duplicateFGGM}$ ) and checks sequence-level Agent-C policy compliance with ${\color[rgb]{0.293,0,0.5117}agentCCheckListWithErrorMsg}$ (dispatching to ${\color[rgb]{0.293,0,0.5117}agentCErrorFGGM}$ on failure). Each FGGM returns a policy-compliant action array ( $arr\langle{\color[rgb]{0,0,1}str}\rangle$ ) via a rejection sampler with $K=5$ and stateful ${\color[rgb]{0.293,0,0.5117}Err_{\Psi_{l}}}$ feedback, so the returned array satisfies the postcondition ${\color[rgb]{0.293,0,0.5117}agentCCheckList}(r,\ tool\_trace,\ domain)$ . The fallback returns a singleton transfer-to-human array and fires on 15.6% (retail) and 21.6% (airline) of instances (Table 8 ).

Category	Hyperparameter	Value
Shared pipeline	Planner search budget ( $\Delta$ )	10
	FGGM rejection-sample budget ( $K$ )	5
	In-context examples	3 (2 for $\tau^{2}$ -bench)
GRPO / LoRA (GSM-Symbolic)	Base model	Qwen3-8B
	LoRA rank	16
	LoRA alpha ( $\alpha$ )	32

Appendix

Table 10. Hyperparameter settings for all evaluation tasks.

Task	Method	Input $\downarrow$	Output $\downarrow$	Total $\downarrow$
HumanEvalDafny	Baseline (Claude Sonnet 4.5)	860	639	1,499
	DafnyBench	2,254	1,836	4,090
	SEVerA	2,740	2,279	5,019
DafnyBench	Baseline (Claude Sonnet 4.5)	925	836	1,761
	DafnyBench	3,419	1,968	5,387
	SEVerA	4,123	2,302	6,425

Appendix

Table 11. Average inference token usage per instance (input / output / total), averaged over the test set.

Panel of Figure 17 — Figure 17. Planner LLM prompt template. The planner receives this prompt at each search–verify–learn iteration, with placeholders filled from the task specification and feedback from the previous iteration.

Agentic Code Generation

Agentic code generation uses AI agents to plan, write, test, and revise executable programs with tools and feedback.

See all 121 papers

Sep 16, 2026

MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs

LLM coding agents now generate complex programs at a scale that makes thorough human review increasingly difficult, raising the risk of safety and security failures. Common approaches, including fuzz testing, static analysis, and LLM-as-a-Verifier, can detect many failures but struggle to cover all possible edge cases. Formal verification addresses this by providing machine-checkable guarantees over specified properties, but traditionally demands substantial manual specification and proof engineering. We introduce a unified multi-agent framework, MAGS, that generates executable programs with formal safety guarantees, using Dafny as a verification-aware intermediate representation where safety properties can be mechanically checked. MAGS formalizes and freezes human-audited APIs and safety requirements, translates generated code into Dafny, repairs violations using verifier feedback, and compiles verified programs back into executable code. We evaluate MAGS on 100 CUDA kernels, 100 terminal scripts, and 20 robotic-arm tasks. Across all 220 examples, it achieves a 100% success rate in producing programs with non-trivial safety guarantees against frozen specifications. Independent safety and functional evaluations further show strong performance across all three domains, while revealing failures when the auto-formalized semantics do not fully capture the target behavior.

Albert Wu, Nicholas Roberts, Tzu-Heng Huang +5

University of Wisconsin-Madison · Princeton University

Multi-Agent LLM Systems Formal Verification Agentic Code Generation Autoformalization LLM Agent Safety

Ask PDF

Oct 8, 2026

VEPA: Verified Evolving Formal Policy for Lifelong LLM Agent Guardrails

LLM agents increasingly operate over sensitive resources, such as private documents and mutable system states, which can create serious safety and security risks. Runtime guardrails should therefore make inspectable, reproducible, and deterministic allow or refuse decisions before potentially irreversible agent actions are executed. However, safety and security requirements are rarely complete before deployment, so guardrails need to keep adapting as new risks emerge. Existing adaptive guardrails learn from deployment experience, but they usually apply safety policies through LLM inference, which can lead to inconsistent decisions and ambiguous policy interpretations. Formal guardrails, on the other hand, enforce policies deterministically, but they usually rely on pre-deployment or task-specific policies and have no mechanism to adapt to newly observed risks. We introduce VEPA, a framework for the verified evolution of formal agent guardrails. VEPA represents the guardrail as a formal policy of executable symbolic rules over typed agent events. During deployment, we use an LLM guided by deployment feedback to propose policy patches that fix newly observed failures while preserving previously correct behavior. Then, a deterministic verifier only accepts policies that are structurally valid and conflict-free. Finally, an evidence-aware authority layer activates a verified rule only when it has enough supporting evidence, so uncertain updates cannot directly affect guardrail decisions. Across ASSEBench-Safety, ASSEBench-Security, and ATBench, VEPA consistently outperforms baselines while expanding the scope of deterministic formal-policy enforcement. These gains also hold under more challenging deployment conditions, including mixed streams, corrupted feedback, and longer horizons.

Duy Nguyen, Lesly Miculicich, Bhavana Dalvi Mishra +5

Google Cloud AI Research · University of North Carolina at Chapel Hill · Google DeepMind

LLM Guardrails Runtime Enforcement for AI Agents LLM Agent Safety

Ask PDF

May 26, 2026

Automating Formal Verification with Agent-Guided Tree Search

Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production. Recent large language models can accelerate this work, and recent benchmarks measure their ability to translate specifications into code and machine-checked proofs of correctness. This thesis evaluates the state of such LLM-driven verified-code generation ("vericoding") in Lean and develops search-based methods for improving verification performance. We first reproduce a subset of the vericoding-benchmark Lean leaderboard on a current cross-vendor model pool, finding that non-reasoning performance remains roughly steady on US closed-source models while open-weight models have slightly improved. We update the iterative methodology of vericoding-benchmark with an agentic loop equipped with mathlib search, finding that model performance greatly improves and scales with agent budget. GPT-5.4 nearly saturates the benchmark at 95.0% on 423 specs with

K=50

LLM calls. We then design two agent-directed tree-search formulations: a state-based orchestrator that branches on partial-proof states, and a context-based orchestrator that branches on full subagent contexts. Compared against the agent baseline, the context-based design solves a wider range of intermediate-difficulty specs at lower token cost, while the agent baseline retains an advantage on the hardest specs, where uninterrupted iteration matters most. We conclude that search structure has selective advantages over a strong agent baseline, and that more challenging benchmarks drawn from modern code are important to measure and drive further progress in automated formal verification. Code available upon request by contacting the author at [email protected].

Leo Yao

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

Code Generation LLM-Based Program Synthesis Formal Verification LLM Agents Code Generation Evaluation Verified Code Generation

Ask PDF

Abstract

Agentic Code Generation

Explore similar work

MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs

VEPA: Verified Evolving Formal Policy for Lifelong LLM Agent Guardrails

Automating Formal Verification with Agent-Guided Tree Search