Self-evolving network verifiers

This paper proposes a vision and provides early evidence for automatically evolving symbolic network verifiers so that their control-plane models faithfully capture actual network behavior, without requiring human experts to hand-encode every protocol and vendor implementation.

The paper begins by noting that while symbolic network verifiers can reason about correctness across vast spaces of routing inputs and failures, they only work for the protocols and features an expert has encoded by hand. The authors state: "Creating and maintaining a faithful model of the control plane is both difficult and never-ending, since no written source specifies perfectly what a network does: vendor implementations deviate from the RFCs, and behaviour shifts with releases. They cite a survey of network operators where the most frequently stated deterrent is that existing tools do not support the protocols and features their networks run."

The authors argue that the problem is not relying upon a model but that humans write it. They propose that the model should instead evolve automatically to faithfully capture the actual network behaviour.

The key insight is to leverage the only source that specifies it unambiguously: the router software itself. The paper describes a counterexample-guided synthesis loop where:

1. A coding agent proposes extensions to the verifier's symbolic encoding

2. A trusted oracle (e.g., emulated routers) supplies ground-truth routing state

3. The agent iteratively refines the network model using each disagreement with the oracle

The specification, in short, is the network you run, not the one the standards describe.

The paper describes how to test a symbolic model against an oracle using two SMT queries:

Soundness: Does the generated SMT model reject a routing state that is observed through the Oracle O? This is checked by asking whether the symbolic model can match the Oracle's routing state (should be satisfiable).

Completeness: Does the generated SMT model accept a routing state that cannot be observed through the Oracle O? This is checked by asking whether the model can disagree with the Oracle's state (should be unsatisfiable).

The loop follows counterexample-guided inductive synthesis (CEGIS), with an LLM as the inductive synthesizer, and with the specification that would ordinarily bound the search replaced by the Oracle. Two agents close the loop:

• Coding Agent: continually refines the verifier's symbolic encoding

• Test Generator: extends the scenario corpus

The loop continues until every scenario passes and the Test Generator can produce a new scenario that the encoding and Oracle have not yet been checked against.

The authors implemented the loop on a 3,000-line Rust SMT verifier and gave it three extension tasks:

1. OSPF areas — Both agents independently converged on the same formulation defining symbolic per-area distances and composed them into inter-area distances dependent on link availability.

2. BGP route reflection (RFC 4456) — "Both agents converged on FRR's decision process, even on a detail that deviates from the route reflection RFC: in Batfish, FRR compares cluster-list length right after the IGP-metric step, ahead of the originator-ID comparison, whereas RFC 4456 §9 prescribes the opposite order. The agents adapted to the FRR logic only through counterexamples authored by the Test Generator."

3. L3VPN over EVPN — Both agents converged on the encoding shown, including all eight terms of the decision process. Notably, a prefix advertised from two sites has a different best route at its origin than in the rest of the network, because a router privately prefers its own routes through an attribute that never leaves the router.

The runs converged for tens of dollars and 100–250 agent steps per feature, with final passing tests of 544/544, 648/648, 600/600, 600/600, 596/596, and 582/582 across six runs. However, runs with Haiku 4.5 as the Coding Agent failed to converge on any of the three tasks.

Tests must co-evolve with the model: Passing the current corpus is thus a fixed point of repair, not of correctness: each repaired model has behaviour that only fresh, code-aware tests can probe. The Test Generator invents scenarios targeting logic that the 316 never stressed and some promptly failed.

Performance matters: Consistency with the oracle is the main signal that drives the loop... But a verifier has (at least) two different requirements: correctness, a hard constraint that admits no tradeoff, and performance, a soft objective. The authors found that verifiers that pass the same tests can differ in efficiency by orders of magnitude. For OSPF areas, one agent's encoding cannot answer the query within 20 minutes at 18 routers while another takes 0.16 seconds. When they resumed a converged run with a generic instruction that the encoding must also scale, the agent independently reinvented the ABR restriction: correctness held at every step (544/544 against the oracle), and the once-intractable query now completes in 0.4 s.

The paper proposes four research directions:

1. Systematic testing of verifiers: The need is not ours alone: the operators of Alibaba's production verifier explicitly call for an automated framework that tests a verifier against vendor implementations. The authors ask: Can we prove a verifier to reason correctly across all environments and supported configurations, given cheap access to the ground truth but only for one scenario at a time?

2. Optimizing for performance: A recurring cause is the boundary between what can be precomputed from the configuration... and what must stay symbolic.

3. Reasoning about more properties: Operators also care about transient states, and performance properties still largely remain out of reach.

4. Universal or ad-hoc verifiers: "If a faithful network model costs days and tens of dollars instead of months of expert labour, what should the community maintain: one 'universal' verifier, or a small verifier per network, covering exactly its configuration and re-evolving as it changes? The authors favor the latter, noting that a community corpus of such scenarios would give ad-hoc verifiers the shared validation that universal ones enjoy today."

The paper concludes that Automating model growth shifts the hard problem from writing verification systems to systematically testing them. The authors argue that while a passing run is weaker than a proof, handwritten encodings do not come with proofs either; they are validated with finite test suites, expert review, and hand-maintained comparisons against ground truth.

Based on this paper, here are the specific improvements I can make to AI systems, and what the improved systems can do:

Improvement: I can implement a closed-loop system where an LLM acts as an inductive synthesizer, proposing model extensions, then iteratively refining them against a trusted oracle (e.g., emulated network devices). The system uses SMT-based differential testing to detect both false positives (model accepts impossible states) and false negatives (model rejects real states), then uses those counterexamples to guide the next model revision.

What the improved system can do: Automatically evolve a symbolic verifier's control-plane model to match real vendor behavior (e.g., FRR's BGP decision order deviating from RFC 4456) without human expert intervention, converging in 100–250 agent steps and tens of dollars per feature.

Improvement: I can add a second agent—a Test Generator—that continuously invents new scenarios targeting untested logic paths. This prevents the system from reaching a fixed point of repair where the model passes all existing tests but is still incorrect. The test generator uses code-aware heuristics to probe areas the current corpus never stresses.

Improvement: I can incorporate a performance objective into the synthesis loop. The paper shows that two models passing identical correctness tests can differ by orders of magnitude in query time (e.g., one takes >20 minutes at 18 routers, another 0.16 seconds). I can add a post-convergence optimization phase where the agent is prompted to make the encoding scale while maintaining correctness, using the oracle to verify each optimization step.

Improvement: I can use the oracle not just for validation but as the primary specification source. Instead of relying on RFCs or documentation, the system learns the actual decision process (e.g., BGP route selection order) by generating counterexamples that force the model to match observed routing states. This handles vendor deviations and version-specific behavior.

Improvement: I can run multiple independent coding agents (e.g., different LLM configurations) on the same task and use their convergence as a confidence signal. The paper shows two agents independently converging on the same encoding formulation, which serves as a form of cross-validation. I can also detect when one agent configuration (e.g., Haiku 4.5) systematically fails and flag that for human review or model switching.

Improvement: I can automatically generate and maintain a corpus of differential-testing scenarios (configuration + oracle state pairs) that any verifier can be checked against. This corpus would be continuously extended by test generators across different networks and features.

Symbolic network verifiers can reason about correctness across vast spaces of routing inputs and failures, but only for the protocols and features an expert has encoded by hand. Creating and maintaining a faithful model of the control plane is both difficult and never-ending, since no written source specifies perfectly what a network does: vendor implementations deviate from the RFCs, and behaviour shifts with releases. The burden of constant upkeep ultimately keeps verification out of many networks that need it. We argue that the model should instead evolve automatically to faithfully capture the actual network behaviour. To achieve that, we leverage the only source that specifies it unambiguously: the router software itself. In a counterexample-guided loop, a coding agent proposes extensions to the verifier's symbolic encoding, while a trusted oracle (e.g., emulated routers) supplies the ground-truth routing state. The agent iteratively refines the network model using each disagreement with the oracle. As early evidence, a prototype of this system taught a 3,000-line SMT-based verifier three features it did not support: OSPF areas, BGP route reflection, and L3VPN over EVPN, converging autonomously on models that match the oracle, even noticing vendor-specific behaviour. Automating model growth shifts the hard problem from writing verification systems to systematically testing them; we propose a research agenda for trusting and harnessing automatically evolved verifiers.