SEVerA: Verified Synthesis of Self-Evolving Agents

Detailed Research Summary: SEVerA (Self-Evolving Verified Agents)

As a fastidious researcher, I have meticulously analyzed the provided excerpts from the paper describing SEVerA (Self-Evolving Verified Agents). This framework addresses a critical gap in existing self-evolving LLM agent paradigms—the lack of formal guarantees regarding safety and correctness when synthesized programs are executed autonomously on unseen inputs.

The core innovation of SEVerA lies in transforming the problem of agentic code generation into a constrained learning problem, effectively combining hard formal specifications with soft objectives that capture task utility.

Core Components and Mechanism

The framework operates across three distinct, sequential stages: Search, Verification, and Learning.

1. Formally Guarded Generative Models (FGGM): The Foundation of Guarantees

The central mechanism introduced is the Formally Guarded Generative Model (FGGM). This component allows the planner LLM to specify precise input-output contracts for every invocation of a parametric generative model (which can include LLMs, smaller neural networks, or external tools like SMT solvers). These contracts are expressed using first-order logic.

Crucially, each FGGM call is not simply executed; it is automatically wrapped in a mechanism that ensures correctness:

• It employs a rejection sampler guided by a checker function (checkA).

• It includes a verified fallback program (f d).

This structure guarantees that every returned output satisfies the specified contract for any input and any parameter setting of the underlying model. This ensures formal correctness is maintained at the generation step.

2. The Three-Stage SEVerA Framework:

• Search: The planner LLM synthesizes candidate parametric programs. These candidates are constructed using FGGM definitions, meaning they inherently contain calls to models that are formally guarded by their respective contracts (l).

• Verification: This stage is where the formal guarantees are rigorously enforced. The language's built-in verifier is employed to prove that the sampled programs satisfy all specified contracts over all possible parameter values of the embedded parametric model calls. This verification step reduces the complex problem to an unconstrained learning problem.

• Learning: With correctness guaranteed by the Verification stage, SEVerA applies scalable gradient-based optimization (including GRPO-style fine-tuning for LLMs) to improve the soft objectives (task utility). The optimization is guided by an augmented objective function that incorporates both task-specific loss and local conformance losses derived from each FGGM contract. This allows for parameter tuning without sacrificing the formal correctness established earlier.

Formal Guarantees and Soundness

The paper provides robust theoretical backing for the framework's reliability:

• Soundness (Theorem 5.4): It is formally proven that any agent returned by SEVerA satisfies its behavioral specification for all inputs and all parameter values of the underlying model.

• Sufficient Condition for Existence (Theorem 5.5): A key result establishes a sufficient condition under which a verified agent exists. This condition ensures that the resulting verified agent satisfies the hard constraints while incurring no greater task loss than any unconstrained generative model starting from its initial parameters, with strict improvement whenever the unconstrained model violates the specification.

Key Contributions and Performance Metrics

The paper asserts several significant contributions:

1. FGGM Introduction: Defining local contracts (l, l) via first-order logic to enforce formal input-output specifications on model calls, applicable to both open and closed-source models.

2. SEVerA Framework: Introducing the first self-evolving agent synthesis algorithm with verifiable guarantees, structured around the Search to Verify to Learn loop.

3. Theoretical Proofs: Establishing the soundness of SEVerA and providing a condition for guaranteed existence of verified agents that meet performance thresholds.

Empirical Validation:

The framework was evaluated across four challenging benchmarks: LLM-Assisted Program Verification (DafnyBench), Agentic Tool Use (tau2-bench), Symbolic Math Synthesis (GSM-Symbolic), and Constrained Symbolic Regression.

The results are highly compelling:

• Zero Constraint Violations: SEVerA consistently achieves zero constraint violations on held-out test inputs across all tasks.

• Superior Performance: It simultaneously improves task performance over every baseline (unconstrained and state-of-the-art agents). Specific metrics include a 97.0% verification rate on HumanEvalDafny (compared to 86.9% for the best baseline) and achieving a 52.6% pass rate on tau2-bench’s airline domain using Qwen3-8B.

Conclusion for High-Stakes Research

SEVerA represents a significant methodological leap by bridging the gap between powerful, autonomous agent synthesis and rigorous formal verification. By embedding formal logic directly into the model invocation process via FGGM, and coupling this with a three-stage loop (Search/Verify/Learn), the authors have successfully engineered an agentic system that is provably safe while still leveraging gradient-based optimization to achieve state-of-the-art performance. The active pruning of the search space by formal constraints is demonstrated not just as a safety feature, but as a mechanism that steers synthesis toward higher-quality agents. This level of formal guarantee combined with empirical superiority makes SEVerA a highly valuable contribution to the field of reliable AI agent development.

1. Formal Behavioral Guarantees: The improved system can synthesize agent programs that are provably correct for all inputs and parameter settings, as stated in every returned output satisfies the specified contract for any input and any parameter setting of the underlying model. This eliminates failures where agents cheat by subtly modifying the input program (e.g., altering variable initializations) so that the modified program with proposed annotations passes verification.

2. Constraint-Guided Search Pruning: The system utilizes formal constraints to prune the space of candidate programs, steering synthesis toward higher-quality agents, ensuring that only programs satisfying the hard behavioral specifications are considered, rather than relying solely on soft performance metrics.

3. Verifiable Local Contracts (FGGM): By introducing Formally Guarded Generative Models (FGGM), the system binds each generative model call to local input–output contracts (Φl, Ψl) and uses a verified fallback, ensuring that even if the underlying parametric model is tuned, the contracts hold because the contract preservation holds over all parameters θ ∈ Θ of the underlying parametric model.

4. Scalable Performance Improvement: The system can improve task performance while maintaining correctness by applying gradient-based optimization to tune parameters guided by a composite loss function: The augmented objective, which includes a local conformance loss for each FGGM call, is defined in Eq. 21. This allows it to achieve gains from both global tuning and local conformance tuning, such as the 12.8% accuracy gain seen in GSM-Symbolic tasks.

5. Domain-Specific Policy Enforcement: For agentic tool use, the system can enforce complex policies by using formal specifications to govern agent actions at each step, ensuring that the Agent-C checker verifies whether the next proposed tool call complies with the defined formal policy before it is executed. This eliminates violations on domain rules like refund eligibility and booking-modification rules.

6. Adaptive Error Recovery: The system implements a dynamic search loop where, upon verification failure, it dispatches to specialized FGGM calls—such as the Error FGGM which provides guidance on timeout, lemma, invariant, or the Verifier Error FGGM which suggests specific fixes—to iteratively correct the program structure.

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 (τ squared-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.