SEVerA: Verified Synthesis of Self-Evolving Agents
Debangshu Banerjee, Changming Xu, Gagandeep Singh
2026-04-09
Summary
This paper introduces a new way to build self-improving AI agents, focusing on making sure these agents are both effective and safe. It's about creating AI that can write and refine its own code to solve problems, but with built-in checks to prevent errors or harmful behavior.
What's the problem?
Currently, AI agents that evolve themselves are really good at getting better at tasks like fixing computer programs or making scientific discoveries. However, there's a big risk because these agents operate on their own and we don't have any solid guarantees that they'll always work correctly or safely. If an agent makes a mistake, especially when dealing with real-world situations, it could cause problems. The core issue is a lack of formal verification – a way to mathematically prove the agent will behave as expected.
What's the solution?
The researchers developed a system called SEVerA, which stands for Self-Evolving Verified Agents. It works in three steps. First, it *searches* for possible programs the agent could use. Then, it *verifies* that these programs will always meet certain safety rules, no matter what. This verification step is done using a special technique called 'Formally Guarded Generative Models' which essentially puts a safety net around each part of the agent's code. Finally, it *learns* to improve the agent's performance while still making sure it stays within those safety boundaries. They use standard AI learning techniques, but with the added constraint of maintaining correctness.
Why it matters?
This research is important because it shows that we can build AI agents that are not only powerful but also reliable and secure. By formally guaranteeing the agent's behavior, we can trust it to operate autonomously without fear of unexpected or harmful outcomes. The results demonstrate that adding these safety checks doesn't hinder performance; in fact, it can actually lead to *better* solutions because it guides the agent towards more robust and well-defined strategies.
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.