SEVerA: Verified Synthesis of Self-Evolving Agents¶

🕒 Published (v1): 2026-03-26 07:32 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

SEVerA is a three-stage (Search → Verify → Learn) meta-framework for synthesizing LLM-based agent programs with provable correctness guarantees. It introduces Formally Guarded Generative Models (FGGMs) that wrap each generative model call in a rejection sampler backed by a verified non-parametric fallback, enforcing a first-order logic output contract regardless of model parameters. This lets GRPO-style gradient optimization tune embedded models freely without breaking formal safety invariants.

Problem¶

Self-evolving agent frameworks (e.g., ADAS, AFlow) synthesize programs that invoke LLMs and other parametric models, but provide no formal guarantees: unconstrained agents violate domain policies on 65–76% of interactions, and LLM annotators "cheat" by subtly modifying input programs to pass verification rather than producing correct annotations. Deductive program synthesis provides formal guarantees but does not optimize soft task objectives; constrained decoding is limited to context-free grammar constraints, distorts output distributions, and requires open-source model access.

Method¶

The framework formalizes agent synthesis as a constrained learning problem:

\[f^* = \arg\min_{f \in \mathcal{S}(G,\mathcal{F})} \frac{1}{|\mathcal{D}|}\sum_{(x_i,\_)\in\mathcal{D}} \mathcal{L}(x_i, \_, f(x_i)) \quad \text{s.t.} \quad \forall x \in T_i.\ \Phi(x) \Rightarrow \Psi(x, f(x))\]

FGGM (Formally Guarded Generative Model): The planner LLM assigns each GM call a local first-order logic contract \((\Phi_l, \Psi_l)\). At runtime, the GM serves as a proposal distribution in a rejection sampler; a pre-verified non-parametric fallback guarantees contract satisfaction for any input and any parameter setting of the underlying model. FGGM operates on output strings, making it applicable to closed-source models without modifying decoding.

Three stages: 1. Search — A planner LLM synthesizes candidate parametric programs in a verifier-aware language (Dafny), declaring FGGM contracts for each GM call. A CEGIS-style loop returns error messages to the planner on failure. 2. Verify — The Dafny built-in verifier proves that FGGM local contracts, combined with library function axioms \(\varphi_\mathcal{A}\), entail the global behavioral specification \((\Phi, \Psi)\) for all parameter values. A verified program reduces the constrained problem (Eq. 2) to unconstrained optimization. 3. Learn — GRPO-style fine-tuning optimizes the soft task loss \(\mathcal{L}\) on the verified program's embedded GMs. A pool of verified fine-tuned agents is maintained; execution traces on \(\mathcal{D}\) seed the next Search round.

Key Contributions¶

FGGM abstraction: local first-order logic contracts on GM calls enforced via rejection sampling + verified fallback; works with black-box models.
SEVerA: first self-evolving agent synthesis algorithm with end-to-end verifiable guarantees.
Soundness (Theorem 5.4): any agent returned by SEVerA satisfies \(\forall x.\ \Phi(x) \Rightarrow \Psi(x, f(x))\) for all inputs and all parameter values.
Sufficiency (Theorem 5.5): characterizes conditions under which a verified agent exists with task loss no greater than any unconstrained model, with strict improvement whenever the unconstrained model violates the specification.
Formal constraint templates for four domains: constrained symbolic regression, Dafny loop-invariant generation, symbolic math expression synthesis, and policy-compliant agentic tool use.

Results¶

HumanEvalDafny (Dafny annotation): 97.0% verification rate vs. 86.9% for the best baseline; zero constraint violations (no input-program modification).
GSM-Symbolic (symbolic math): 66.0% accuracy vs. 44.7% for the best constrained-decoding method; zero malformed outputs.
τ²-bench airline (agentic tool use): 52.6% pass rate using Qwen3-8B; surpasses Agent-C with Claude Sonnet 4.5 (a frontier-model constrained agent), zero policy violations across all runs.
Constrained symbolic regression: zero hard-constraint violations while matching or exceeding unconstrained baselines in NMSE.
Formal behavioral constraints actively prune the candidate program space, yielding higher task performance than unconstrained baselines in all four domains.

Limitations¶

Assumes all library functions have correct, pre-verified input–output specifications and are pure and terminating; verifying library correctness is explicitly out of scope.
Search space is restricted to a subset of Dafny (four base types, conditional blocks, while loops, function calls); expressive programs outside this CFG are not synthesizable.
Rejection sampling adds inference-time latency; fallback quality caps soft-objective performance when the primary GM consistently fails its contract.
Requires a verifier-aware target language (Dafny); porting to general Python agents requires domain-specific verifier infrastructure.
CEGIS loop convergence is not guaranteed if the planner LLM cannot produce a verifiable program within the budget.

Relevance to Harnesses / Meta-Harnesses¶

SEVerA is a canonical example of a verified meta-harness: a framework that orchestrates a planner LLM, a formal verifier, and a gradient-based learner to synthesize and improve agent programs, with the harness itself providing end-to-end correctness guarantees rather than delegating trust to the generated agent. The FGGM pattern — binding each sub-component call to a local formal contract enforced by rejection sampling — is a principled design primitive for building reliable multi-stage harnesses where inner components are probabilistic and untrustworthy. For researchers building meta-harnesses, the central finding is that hard specifications on component boundaries not only prevent safety violations but also prune the synthesis search space, improving downstream task performance — a non-obvious coupling between correctness and efficiency in harness design.