SEVerA: Verified Self-Evolving Agents with Specification Guidance

Recent works have demonstrated the effectiveness of self-evolving LLM agents across a range of tasks, including program repair and scientific discovery. In this paradigm, a planner LLM synthesizes an agent program (e.g., a model harness) that invokes parametric models, including LLMs, smaller neural networks, and external tools, which are then tuned for each task to improve performance. However, existing self-evolving frameworks provide no formal guarantees of safety or correctness, even though the synthesized programs are executed autonomously on unseen inputs. We formulate agentic code generation as a constrained learning problem that combines hard formal specifications with soft objectives capturing task utility. We introduce Formally Guarded Generative Models (FGGM), in which each model call is wrapped in a rejection sampler with a verified fallback, ensuring that the model always satisfies a first-order output contract for any input and parameter setting. Building on FGGM, we present SEVerA (*S*elf-*E*volving *Ver*ified *A*gents), a three-stage *Search$\to$Verify$\to$Learn* framework. We evaluate SEVerA on policy-compliant agentic tool use ($\tau^2$-bench), automated program verification, scientific discovery, and symbolic math synthesis. SEVerA achieves zero constraint violations while improving task performance over unconstrained and state-of-the-art baselines, demonstrating that formal behavioral constraints both prune bad candidate programs and steer synthesis toward higher-quality agents.