# SEVerA: Verified Synthesis of Self-Evolving Agents

arXiv: https://arxiv.org/abs/2603.25111 · HTML: https://mlsanity.com/paper/2603.25111/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 30 of its 51 references that are in the map.
- First posted on arXiv 26 Mar 2026.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)
- Synthetic data and self-improvement for LLMs / [Self-evolving LLM agents](https://mlsanity.com/synth/self-evolving-llm-agents/)

## Builds on (most cited first, 30 of 30)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Voyager: An Open-Ended Embodied Agent with Large Language Models](https://mlsanity.com/paper/2305.16291/) (2023)
- [ViperGPT: Visual Inference via Python Execution for Reasoning](https://mlsanity.com/paper/2303.08128/) (2023)
- [Executable Code Actions Elicit Better LLM Agents](https://mlsanity.com/paper/2402.01030/) (2024)
- [Prompting Is Programming: A Query Language for Large Language Models](https://mlsanity.com/paper/2212.06094/) (2022)
- [Symbolic Learning Enables Self-Evolving Agents](https://mlsanity.com/paper/2406.18532/) (2024)
- [RedCode: Risky Code Execution and Generation Benchmark for Code Agents](https://mlsanity.com/paper/2411.07781/) (2024)
- [Neuro-Symbolic Program Synthesis](https://mlsanity.com/paper/1611.01855/) (2016)
- [SynCode: LLM Generation with Grammar Augmentation](https://mlsanity.com/paper/2403.01632/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [ImpossibleBench: Measuring LLMs' Propensity of Exploiting Test Cases](https://mlsanity.com/paper/2510.20270/) (2025)
- [FlowReasoner: Reinforcing Query-Level Meta-Agents](https://mlsanity.com/paper/2504.15257/) (2025)
- [WebEvolver: Enhancing Web Agent Self-Improvement with Coevolving World Model](https://mlsanity.com/paper/2504.21024/) (2025)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Grammar-Aligned Decoding](https://mlsanity.com/paper/2405.21047/) (2024)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [HOUDINI: Lifelong Learning as Program Synthesis](https://mlsanity.com/paper/1804.00218/) (2018)
- [CRANE: Reasoning with constrained LLM generation](https://mlsanity.com/paper/2502.09061/) (2025)
- [Type-Constrained Code Generation with Language Models](https://mlsanity.com/paper/2504.09246/) (2025)
- [Enforcing Temporal Constraints for LLM Agents](https://mlsanity.com/paper/2512.23738/) (2025)
- [IterGen: Iterative Semantic-aware Structured LLM Generation with Backtracking](https://mlsanity.com/paper/2410.07295/) (2024)
- [Shape-constrained Symbolic Regression -- Improving Extrapolation with Prior Knowledge](https://mlsanity.com/paper/2103.15624/) (2021)
- [DINGO: Constrained Inference for Diffusion LLMs](https://mlsanity.com/paper/2505.23061/) (2025)
- [SEEA-R1: Tree-Structured Reinforcement Fine-Tuning for Self-Evolving Embodied Agents](https://mlsanity.com/paper/2506.21669/) (2025)
- [ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models](https://mlsanity.com/paper/2509.00360/) (2025)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples](https://mlsanity.com/paper/1611.07502/) (2016)
- [Takedown: How It's Done in Modern Coding Agent Exploits](https://mlsanity.com/paper/2509.24240/) (2025)
- [Semantics-Guided Synthesis](https://mlsanity.com/paper/2008.09836/) (2020)
- [Shape-constrained Symbolic Regression with NSGA-III](https://mlsanity.com/paper/2209.13851/) (2022)

## Built on by (most cited first, 8 of 8)

- [Safety in Self-Evolving LLM Agent Systems: Threats, Amplification, and Case Studies](https://mlsanity.com/paper/2606.23075/) (2026)
- [Selection Without Signal, Recovery Through Expression: A Measurement Study of Post-Hoc Falsification Operators for Frozen Small Code Models](https://mlsanity.com/paper/2606.16999/) (2026)
- [EvoUndo: Recoverability-Constrained Self-Evolution for LLM Agent Harnesses](https://mlsanity.com/paper/2608.28363/) (2026)
- [Forethought: Verifiable Reasoning from Neurosymbolic Primitive Programming](https://mlsanity.com/paper/2607.04096/) (2026)
- [Program Learning with Verifiable Rewards: Symbolic Backpropagation for Post-Training LLMs](https://mlsanity.com/paper/2608.28421/) (2026)
- [Authorization for Self-Modifying AI Agent Populations: Conserving Authority across Replacement, Forking, and Rollback](https://mlsanity.com/paper/2610.00347/) (2026)
- [WorkflowOps: Learning Agent Collaboration Priors for Multi-Agent Workflow Orchestration](https://mlsanity.com/paper/2610.07860/) (2026)
- [Compiling Expert Procedures into Verified Programs: When a Small Model Is Enough](https://mlsanity.com/paper/2610.19148/) (2026)

## Abstract (arXiv)

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.