Self-evolving network verifiers

Self-evolving network verifiers Ioannis Protogeros

Tibor Schneider

Laurent Vanbever

ETH Zürich Zürich, Switzerland iprotogeros@ethz.ch

ETH Zürich Zürich, Switzerland sctibor@ethz.ch

ETH Zürich Zürich, Switzerland lvanbever@ethz.ch C : configuration space

arXiv:2608.11340v1 [cs.NI] 11 Aug 2026

ABSTRACT 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 counterexampleguided 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.

1

E : environment space

∗

∗

∗

E

∗ ∗ C control-plane verification

∗ ∗

∗

∗

∗

∗

∗

∗

∗ ∗

∗

∗

emulation

all environments within any configuration, a fixed configuration space one environment at a time

∗

self-evolving space grown through oracle-checked scenarios

Figure 1: A self-evolving verifier keeps the symbolic model’s guarantees and grows their coverage, guided by ground-truth observations. Existing verifiers indeed support only the features their authors have manually encoded, which is only a subset of what operators actually run. This is not surprising: accounting for all the different protocols and vendor implementations is a Sisyphean task. (The maintainers of Batfish already report a decade’s worth of extending vendor and protocol support and of chasing undocumented semantics in router software [8].) Worse, extending models is often disproportionately hard because of how protocols interact. For instance, a BGP verifier cannot “only” model the BGP computation across vendors and implementations; it also needs to model the IGP computation logic, again across vendors and implementations, as the BGP’s route selection depends on the IGP costs [4]. These limits have pushed recent works to make radical proposals: in [20], the authors argue that “models will always lag in their ability to faithfully represent the actual control plane”. They propose abandoning the models altogether and instead running the configuration on an emulated network, analysing the resulting data plane directly. Such model-free approaches overcome the limitations of handcrafted models: any feature the router image supports is covered, the image is always up-to-date, and there is no encoding to extend. Foregoing models comes with a high cost, though: the loss of widely applicable guarantees. For a single converged data plane, we can easily reason about properties without using a model; we just run the configuration and then verify correctness over the packet space [18, 19]. But whether the network stays correct across environments (any link failure, any external advertisement) is a question that a single data plane cannot answer. Most of the time, the environment space is huge and combinatorial, making it intractable to

INTRODUCTION

Network verification is remarkably powerful: given only a configuration, modern tools can reason about network behaviours across all possible routing inputs and link failures [4, 6]—at least, in theory. In practice, though, a decade of academic success has not translated (yet) into (vast) industry adoption. In a recent survey of network operators, the most frequently stated deterrent is that existing tools do not support the protocols and features their networks run [20]. As a result, most networks remain unverified and continue to suffer the outages that verification was built to prevent [30]. The reason can be traced to a single artifact: the network control-plane model, which is today built entirely by hand. 1

Ioannis Protogeros, Tibor Schneider, and Laurent Vanbever

enumerate every possible data plane. Relying on a (symbolic) model [6] is precisely what enables control-plane verification to reason about all environments at once. In this paper, we argue that the problem is not relying upon a model but that humans write it. To address this, we describe a vision in which symbolic models automatically evolve to faithfully represent the behaviour of the network they describe (Fig. 1). In this world, models automatically cover new features, adapt to new vendors or software updates, without any expert labour. More importantly, they do so without surrendering the vast guarantees they provide. Realizing this vision is, quite unsurprisingly, difficult. Yet, we believe the recent advances in network emulation, coupled with the advances in LLM-based code generation, make it possible. Concretely, we treat the network model like software under test: we continually compare what the model admits against what the network computes, and let an LLM coding agent repair the model wherever the two disagree. Any procedure that changes the model automatically needs a criterion for when a change is correct [15]. In networking, deriving such a specification is exceedingly difficult because no written source exists that specifies what a network actually does. Protocol implementations diverge from the RFCs [33], vendor documentation is incomplete [8], protocols interact in ways no standard describes [7], and behaviour shifts across even minor releases. The one artifact that fully determines a network’s behaviour is the router software, and unlike a written specification, it can be executed: emulation can therefore answer, for any configuration in one concrete environment, exactly what the model should say. We therefore propose to use this executable ground truth to drive a counterexample-guided synthesis loop: for each configuration and concrete environment, we check that the symbolic model is consistent with the routing state the network computed. Every disagreement becomes a counterexample, and an off-the-shelf coding agent turns counterexamples into candidate repairs (current LLMs have been shown to be effective in various adjacent domains [21, 23, 25, 31]). The specification, in short, is the network you run, not the one the standards describe: in our experiments (§3.1), the agents initially followed RFC 4456’s route-selection order [2], but the ground truth followed a different order [12]; counterexamples guided the agents to it. We present early evidence that our vision works endto-end. On a 3,000-line Rust SMT verifier, this pipeline autonomously added three mechanisms the model did not support: OSPF areas, BGP route reflection, and L3VPN over EVPN, each for a few tens of dollars and with no expert in the loop beyond inspecting the end result. While this approach drastically reduces the cost of obtaining a possibly correct network model, the hard problem shifts from writing verifiers to systematically testing them: what

makes a corpus of tests adequate, and how far can we trust an oracle beyond the tested region? If we can confidently reason about the soundness of an automatically evolved verifier, the implications would be paramount: expanding protocol and property coverage, making verification more accessible and useful to many networks, and thereby shielding them from regularly occurring outages.

2

SELF-EVOLVING VERIFIER

This section makes the vision concrete: we state the problem (§2.1), show how to test a symbolic model against an Oracle (§2.2), close the loop that repairs it (§2.3), and state what a passing run does (and does not) certify (§2.4).

2.1

Problem statement

We are given a set of configurations C, the environments E they may face—link failures, external advertisements—and a verifier V that cannot reason correctly about every scenario (𝑐, 𝑒): a configuration paired with one concrete environment. We also have an Oracle O we trust (a simulator, emulator, or the network itself), which, given a scenario, returns the routing state the network converges to. For simplicity, we consider only networks where this state is unique (otherwise, every notion of agreement below would range over all possible stable routing states [13, 14]). Our goal is to produce an extended verifier V + that agrees with the Oracle on all scenarios. More concretely, the verifier’s model must accept the routing state the Oracle produces and must accept no other. As with any tested system, if a large and varied corpus cannot surface any difference between the model and the Oracle, we trust the model across all configurations in C and environments in E.

2.2

Differentially testing a verifier

A network model produced by a verifier is not directly comparable to the output of a simulator or an emulator; the former is an abstraction over the network control plane across all possible environments, while the latter takes the configuration and one concrete environment as input and produces the routing state. Still, we can query the verifier’s network model to test whether the model is consistent with the routing state calculated by the Oracle for a specific environment. That involves crafting two queries that check for two converse requirements; for a given configuration 𝑐 and environment 𝑒: Soundness: Does the generated SMT model reject a routing state that is observed through the Oracle O? We can effectively check soundness by crafting an SMT query that asks “Given the environment 𝑒, is it possible for the routes in the SMT model to be the same as the ones produced by the Oracle?”. If we denote as 𝑟 each route in the routing table calculated by 2

Self-evolving network verifiers

Seeds

Self-evolving loop latest repair (diff)

Verifier V

more tests needed? → add scenarios {𝑐 ′ , 𝑒 ′ }

+ Scenarios {(𝑐, 𝑒)}

config ∈ C

env ∈ E

Test Generator

Coding Agent tests and report

extends counterexample (𝑐, 𝑒 )

Evolving verifier V

Differential check ?

RT # ≡ 𝑅𝑇 Oracle O Configuration set C

Environment set E

Extended verifier V +

symbolic routing state R T # (𝑐, 𝑒 )

all tests pass ∧ no more tests needed

as two SMT queries (§2.2)

𝑅𝑇 (𝑐, 𝑒 ) concrete routing state

Figure 2: Every disagreement between the symbolic model and the Oracle becomes a counterexample that drives the next repair; the loop ends only when the whole corpus passes and the Test Generator can grow it no further. the Oracle 𝑅𝑇 = O (𝑐, 𝑒), and 𝑟 # its respective symbolic route under the SMT model, then that query would be ! Û # 𝑒∧ 𝑟 = 𝑟 ⇝ (should be sat)

The loop follows counterexample-guided inductive synthesis (CEGIS) [29], with an LLM as the inductive synthesizer [25], and with the specification that would ordinarily bound the search replaced by the Oracle (a form of OGIS [17]). We seed the corpus with scenarios (𝑐, 𝑒) and run the differential test on each of them. A scenario in which either query fails is a counterexample: a configuration and environment in which the encoding and the Oracle disagree. We hand it to the Coding Agent along with the failing query and the Oracle’s routing state; the agent edits the encoding, we recompile, and the entire corpus is re-run so that a fix for one feature cannot regress another. Iteration continues until every scenario passes. Passing the corpus certifies the encoding only on the scenarios it contains, so it is not, on its own, a stopping condition. We therefore ask the Test Generator whether any untested region of the configuration space remains. If it can produce a new scenario that the encoding and Oracle have not yet been checked against, that scenario enters the corpus, and the loop resumes; only when all tests pass, and no further scenario is needed, do we emit the extended verifier V + .

𝑟 ∈𝑅𝑇

Here 𝑟 = 𝑟 # asserts, for a concrete route 𝑟 and its symbolic counterpart at the same (router, destination) slot, agreement on availability and on every route attribute (next hop, local preference, AS-path, and so on). A sat result here exhibits a model assignment matching reality; unsat means the encoding forbids the real state. Completeness: Does the generated SMT model accept a routing state that cannot be observed through the Oracle O? Conversely, we check completeness by querying whether the symbolic encoding can disagree with the Oracle’s state. ! Ü # 𝑒∧ 𝑟 ≠ 𝑟 ⇝ (should be unsat) 𝑟 ∈𝑅𝑇

A sat result here would mean that the model accepts a spurious state, revealing a bug (or an omission) in the encoding.

2.3

The evolution loop

2.4

The differential testing approach above turns a single scenario into a verdict on the current encoding, but a verdict alone does not repair the model. Two agents close the loop (Fig. 2): a Coding Agent that continually refines the verifier’s symbolic encoding, and a Test Generator that extends the scenario corpus.

What a passing run means

A successful test run certifies that, for every scenario in the corpus, the verifier encoding admits the Oracle’s routing state, and no other. Any claim beyond the corpus is inductive, so naturally, there can still be uncaught errors; untested regions of the configuration and environment space may still hide modelling bugs. Furthermore, the symbolic model 3

Ioannis Protogeros, Tibor Schneider, and Laurent Vanbever OSPF areas Coding Agent model Tests (seed→final) Rounds (failing) Agent steps Total cost ($) Lines added Final passing tests

Opus

Sonnet

Route refl. Opus

Sonnet

3.1

L3VPN Opus

Sonnet

Figure 3 distills each converged encoding into the rules the agent effectively added, as faithful abridgements of the agents’ Rust/Z3 code.

316→544 316→648 484→600 484→600 508→596 508→582 7 (3) 9 (1) 5 (1) 4 (0) 13 (3) 11 (2) 95 91 200 173 218 254 41.8 35.8 30.1 18.7 37.2 25.0 288 275 85 152 1162 1060 544/544 648/648 600/600 600/600 596/596 582/582

OSPF areas (Fig. 3i). Both agents independently converged on the same formulation. They defined symbolic per-area distances and composed them into inter-area distances dependent on link availability. Correctly modelling shortest-path calculation under the partitioning of Area 0 was a subtlety that required both agents to refine their code through counterexamples.

Table 1: Every run converged to full agreement with its oracle on an implementation-aware testing suite.

Route reflection (Fig. 3ii). 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 [3], whereas RFC 4456 §9 prescribes the opposite order. Originally, the agents implemented an SMT model from their knowledge of the protocol, so the route decision process followed the RFC. They adapted to the FRR logic only through counterexamples authored by the Test Generator.

remains an abstraction of actual network behaviour, meaning that properties more granular than this abstraction cannot be tested against an emulator. While we recognize that this is weaker than a proof, handwritten encodings do not come with proofs either; they are validated with finite test suites, expert review, and handmaintained comparisons against ground truth (e.g., Batfish against emulated networks [8], Alibaba’s Hoyan continuously against its live WAN [34]), and prominent verifiers ship fidelity bugs regardless [7, 20]. So, irrespective of the paradigm that creates the verifier, there is a need to systematize the testing of such systems, and differential testing [22] against—now cheaper and more accessible—emulators is a step in that direction.

3

What the agents modelled

L3VPN over EVPN (Fig. 3iii). Both agents converged on the encoding shown, including all eight terms of the decision process ≺. There were, however, subtleties in the network that the RFCs do not specify: 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 router software had to reveal such behaviour [12].

EARLY RESULTS

We implemented and ran the loop of §2 on an SMT-based control-plane verifier (∼3000 lines of Rust using Z3 [10]) that models BGP over a flat shortest-path IGP. We gave it three extension tasks for mechanisms it did not model: (i) OSPF areas, (ii) BGP route reflection (RFC 4456), including cluster lists, originator IDs, and their effect on best-path selection; and (iii) L3VPN over EVPN, a feature family the verifier had no notion of. The oracle is hot-swappable, and we used two oracles of different fidelity: Batfish [11] for (i) and (ii), and emulated FRRouting instances (via containerlab) for (iii), where L3VPN support is more complete. A general Coding Agent (Claude Opus 4.8 or Sonnet 5) is tasked with implementing the update to the existing symbolic verifier; the Test Generator is a separate agent (Opus 4.8 throughout) that reads the implementer’s code and existing test cases each round and proposes new scenarios. Table 1 summarizes the runs. For tens of dollars and ∼100– 250 agent steps per feature, every run converged, via oracle counterexamples and internal protocol knowledge, to a verifier that fully agreed with its oracle on a test corpus adversarially grown by the Test Generator. Not every model we tried sufficed: runs with Haiku 4.5 as the Coding Agent failed to converge on any of the three tasks.

3.2

Tests must co-evolve with the model

Figure 4 traces how a run’s corpus and passing checks move together: in each round, the Test Generator tries to grow the corpus with adversarial examples, and each red cross is a round that ended with counterexamples. The runs share a common structure. The verifier’s initial state fails a large fraction of the seed corpus—unsurprisingly so, since a lot of the seed scenarios exercise the very feature being added (e.g., 100 of 316 for OSPF areas)—and the agent repairs against those counterexamples until the seed passes. Had the loop stopped there, the model would look finished. Yet in every run, the Test Generator, reading the converged code, invented scenarios the seed never stressed, and some promptly failed. Figure 5 follows one such trajectory in detail. 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. Our Test Generator finds such tests, but greedily and without guarantees: nothing tells us how far “the Test Generator ran out of ideas” is from “no counterexample exists.” Closing that gap, e.g. by generating adversarial scenarios systematically, with some 4

Self-evolving network verifiers

define

𝐷 (𝑠, 𝑡 ) =

min 𝑥 ∈ ABR(𝑎𝑠 ) 𝑦 ∈ ABR(𝑎𝑡 )

converged 648/648

per-area distances 𝑑𝑎 (𝑢, 𝑣) : symbolic shortest paths over the area-𝑎 links that are up in the environment

tests passed

define

× failing (count)

passing

(i) OSPF areas

𝑑𝑎𝑠 (𝑠, 𝑥 ) + 𝑑 0 (𝑥, 𝑦) + 𝑑𝑎𝑡 (𝑦, 𝑡 )

↩→ Despite leading to the exact same result, Opus considered the min over a much vaster space (§3.3)

544/544

600 400

20 100

8 4

100

200 assert assert

each path segment is reachable within its area an intra-area route, when one exists, beats every inter-area route, regardless of cost

0

3

0

define define assert

CL ← cid (𝑟 ) :: CL ⊲ reflector 𝑟 prepends its cluster ID OID ← sender if unset router 𝑡 admits a route iff OID ≠ 𝑡 ∧ 𝑐𝑖𝑑 (𝑡 ) ∉ CL ⊲ loop rejection

tests passed

per-route attributes: cluster list CL, originator ID OID

⊲ best-path selection

routers 𝑅 , weighted core links 𝐿 , EVPN sessions 𝐸 , VRF attachments, originated prefixes 𝑂

define

𝑑 (𝑢, 𝑣) : shortest paths after deleting failed nodes and links

define define define define define define define define

600/600

525 450

0

51

3

6

(c) Route reflection · Opus

9

0

3

6

9

round

(d) Route reflection · Sonnet

Figure 4: An evolved verifier that passes all tests in a single round might still fail on different inputs.

act (𝑢, 𝑣) ⇔ (𝑢, 𝑣) ∈ 𝐸 ∧ both up ∧ 𝑑 (𝑢, 𝑣) < ∞ ⊲ EVPN session liveness 𝑜 ⇝ 𝑡 : RFC 4456 reflection reachability over act ⊲ overlay RR rt (𝑣) = ASN:VNI if auto, rd (𝑣) = routerID:vrfID if auto ⊲ route target / distinguisher a type-5 route is ⟨rd (𝑜 ), 𝑝, RT (𝑜 ), A (𝑜 ) ⟩ ⊲ RD keys identity ≺ = ¬weight, LP, |ASpath|, origin, MED, eBGP≺iBGP,
IGP cost, router ID ⊲ full decision process ebest (𝑟, rd, 𝑝 ) = min ≺ { 𝑜 : rd (𝑜 ) = rd ∧ 𝑑 (𝑟, 𝑜 ) < ∞ ∧ 𝑜 ⇝ 𝑟 } ⊲ EVPN RIB: selection per (RD, prefix), not across RDs cand (𝑟, 𝑣, 𝑝 ) = { ebest (𝑟, rd, 𝑝 ) : rt imp (𝑟, 𝑣) ∈ RT (𝑜 ) ∧ rd (𝑜 ) ≠ rd (𝑣) } ⊲ leak: import filter + self-RD rejection best (𝑟, 𝑣, 𝑝 ) = min ≺ cand (𝑟, 𝑣, 𝑝 ) ⊲ tenant v4 RIB: cross-RD competition resolved here

Figure 3: The two agents converged to semantically equivalent encodings.

notion of coverage over a targeted scenario space, is, we argue, a core open problem for self-evolving verifiers (§4).

3.3

9

2

round

given

6

600

51

(iii) L3VPN over EVPN

3

(b) OSPF areas · Sonnet

600/600

define

lexicographic minimization along · · · ≻ IGP cost ≻ |CL| ≻ OID ≻ peer ID

9

(a) OSPF areas · Opus

(ii) Route reflection

define

6

Agent writes an OSPF areas model from protocol knowledge alone. 316 starting scenarios: 100 disagree.

Each disagreement is a counterexample: the scenario plus the ground-truth routes. Repairs to 316/316.

Test Generator reads the new code, invents scenarios targeting logic that the 316 never stressed. New tests pass.

Two more rounds add no failing test cases. Converged: 544/544.

Another: area 0 splits in two; the dest. sits in the other segment but is an ABR, so the code requires an impossible all-backbone path while blocking the valid inter-area route: 8 fail. Repaired.

New scenario: two ABRs can each bridge the same area pair. Yet, upon a link failure, the path through the other ABR was not chosen: 4 fail. Repaired.

Figure 5: The Test Generator proposes adversarial scenarios until it cannot invent further ones.

Performance is important too!

Consistency with the oracle is the main signal that drives the loop of §2. But a verifier has (at least) two different requirements: correctness, a hard constraint that admits no tradeoff, and performance, a soft objective the model can satisfy to wildly varying degrees. The oracle enforces only the first on the test corpus; computational tractability is invisible to it. We benchmarked each pair of converged network models on the same query—proving reachability under all singlelink failures—over topologies at growing sizes. Each pair yields the same verdict, yet their costs diverge by orders of magnitude. For OSPF areas, Opus’s encoding considers

vastly more candidate inter-area paths than are actually possible, while Sonnet derives each area’s border routers from the configuration and admits only paths through them. The redundant computations compound with scale: at just 18 routers, Opus’s encoding cannot answer the query within 20 minutes, while Sonnet’s takes 0.16 s. For L3VPN at 17 routers, Sonnet’s model takes 143 s, whereas Opus’s takes 0.9 s (all measurements are means over 10 runs). To test whether the loop can also pursue the performance objective, we resumed the converged Opus OSPF run with a single generic instruction (the encoding must also scale) and 5

Ioannis Protogeros, Tibor Schneider, and Laurent Vanbever

a cheap size signal (SMT DAG nodes), with no hint at the underlying anti-pattern. In two rounds 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. A tangible gap remains, however: Sonnet’s encoding is still over 2× faster on the same proof, so even within verifiers with similar network models and the same end results, performance may vary significantly.

4

cause is the boundary between what can be precomputed from the configuration (e.g., an area’s border routers) and what must stay symbolic (distances under failures) [5]. That boundary moves with the query: a reachability check on a fixed topology has no need for symbolic distances. Taken to its limit, concretizing everything is simply enumeration (one emulation per environment) which, for spaces like all single-link failures, may well beat a symbolic query, and certainly beats an unfortunate SMT encoding (§3.3). If deriving a model is cheap, a verifier need not fix this boundary once; it could adapt specific calculations to use full symbolic reasoning or plain enumeration.

RESEARCH AGENDA

Systematic testing of verifiers. The system in §2 drastically cuts the cost of writing a verifier, leaving only the task of rigorously testing one. 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 and diagnoses the causes of divergence [34]. While our Test Generator does expose failures by probing logic that the previous test suite never stressed, it cannot guarantee that every corner case is covered. Tests must cover two spaces: configurations and network environments. Regarding configurations, we need ones that surface discrepancies between the network model and groundtruth behaviour, and such scenarios are sparse: validating the order of a decision process at step 𝑘 requires routes with equal attributes on all previous steps, as in the routereflection tie-break of §3.1. Our Test Generator greedily finds such scenarios, with no notion of exhaustion. Recent work [35] shows adversarial inputs uncover correctness and performance bugs in AI-evolved programs (e.g., [24, 26]) that their original evaluation suites miss. Similarly, an evolved verifier should be tested on adversarial scenarios. Regarding environments, the verifier’s guarantees must hold over all of E, but each differential test checks a single point of it (the same limitation that model-free verification faces [20]). Coverage metrics for network configuration tests exist [32], but they do not extend to network models that reason symbolically over environment spaces. Formal verification suggests what such a metric could look like: in model checking, a part of the model is considered covered only if mutating it reverses the verdict of some check [9, 16]. Transferred here, if mutating a piece of the model changes no scenario’s outcome, then the tests never exercised that piece of logic. A fundamental research question remains: 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?

Reasoning about more properties. The loop evolves toward whatever its oracle tests against. In this case, converged routing state (§2.2). However, operators also care about transient states [27], and performance properties still largely remain out of reach: general formal models for network performance scale poorly [1], and verifying specific properties, such as worst-case link loads, requires modelling and optimizing entire systems by hand [28]. Emulation already observes transient states, link loads, and convergence times, so the question remains: how can we use these signals to effectively steer the creation of a faithful and tractable network model? 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? Our results favour the latter, since each verifier automatically adapts to vendor-specific behaviour, whereas general configuration analysis tools like Batfish must encode all possible vendor-dependent behaviours and select the applicable one per configuration. What the universal verifier offers instead is more comprehensive validation: every scenario tests the same code, whereas a per-network verifier is tested only in its own domain. Yet a hard scenario found by one network’s loop is an oracle-checked, reusable test for any verifier that covers the same features. A community corpus of such scenarios would give ad-hoc verifiers the shared validation that universal ones enjoy today.

REFERENCES [1] Mina Tahmasbi Arashloo, Ryan Beckett, and Rachit Agarwal. 2023. Formal Methods for Network Performance Analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23). USENIX Association, Boston, MA, 645–661. https://www.usenix. org/conference/nsdi23/presentation/tahmasbi [2] Tony Bates, Enke Chen, and Ravi Chandra. 2006. BGP Route Reflection: An Alternative to Full Mesh Internal BGP (IBGP). RFC 4456. https: //doi.org/10.17487/RFC4456 [3] Batfish Project. 2025. Batfish v2025.07.07, BgpRib.java. https://github.com/batfish/batfish/blob/v2025.07.07/projects/ batfish/src/main/java/org/batfish/dataplane/rib/BgpRib.java.

Optimizing for performance. The oracle enforces correctness on the corpus, yet computational tractability is invisible to it, and §3.3 showed that verifiers that pass the same tests can differ in efficiency by orders of magnitude. A recurring 6

Self-evolving network verifiers

[4] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM ’17). 155–168. https://doi.org/10.1145/ 3098822.3098834 [5] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2018. Control plane compression. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (Budapest, Hungary) (SIGCOMM ’18). Association for Computing Machinery, New York, NY, USA, 476–489. https://doi.org/10.1145/3230543.3230583 [6] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2020. Abstract Interpretation of Distributed Network Control Planes. Proceedings of the ACM on Programming Languages 4, POPL, Article 42 (2020). [7] Rudiger Birkner, Tobias Brodmann, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2021. Metha: Network Verifiers Need To Be Correct Too!. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 99–113. https://www. usenix.org/conference/nsdi21/presentation/birkner [8] Matt Brown, Ari Fogel, Daniel Halperin, Victor Heorhiadi, Ratul Mahajan, and Todd Millstein. 2023. Lessons from the evolution of the Batfish configuration analysis tool. In Proceedings of the ACM SIGCOMM 2023 Conference (New York, NY, USA) (ACM SIGCOMM ’23). Association for Computing Machinery, New York, NY, USA, 122–135. https://doi.org/10.1145/3603269.3604866 [9] Hana Chockler, Orna Kupferman, and Moshe Vardi. 2003. Coverage Metrics for Formal Verification. Vol. 8. 111–125. https://doi.org/10. 1007/978-3-540-39724-3_11 [10] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. Vol. 4963. 337–340. https://doi.org/10.1007/978-3-540-788003_24 [11] Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A general approach to network configuration analysis. In Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (Oakland, CA) (NSDI’15). USENIX Association, USA, 469–483. [12] FRRouting Project. 2026. FRRouting 10.6.1, bgpd/bgp_route.c, function bgp_path_info_cmp. https://github.com/FRRouting/frr/blob/frr10.6.1/bgpd/bgp_route.c. [13] Lixin Gao and J. Rexford. 2001. Stable Internet routing without global coordination. IEEE/ACM Transactions on Networking 9, 6 (2001), 681– 692. https://doi.org/10.1109/90.974523 [14] T.G. Griffin, F.B. Shepherd, and G. Wilfong. 2002. The stable paths problem and interdomain routing. IEEE/ACM Transactions on Networking 10, 2 (2002), 232–243. https://doi.org/10.1109/90.993304 [15] Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis. Foundations and Trends® in Programming Languages 4 (07 2017), 1–119. https://doi.org/10.1561/2500000010 [16] Y. Hoskote, T. Kam, Pei-Hsin Ho, and Xudong Zhao. 1999. Coverage estimation for symbolic model checking. In Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361). 300–305. https://doi. org/10.1109/DAC.1999.781330 [17] Susmit Jha and Sanjit A. Seshia. 2016. A Theory of Formal Synthesis via Inductive Learning. arXiv:1505.03953 [cs.AI] https://arxiv.org/ abs/1505.03953 [18] Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). USENIX Association, San Jose, CA, 113–126. https://www.usenix. org/conference/nsdi12/technical-sessions/presentation/kazemian

[19] Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). USENIX Association, Lombard, IL, 15–27. https://www.usenix.org/conference/nsdi13/technicalsessions/presentation/khurshid [20] Alexander Krentsel, Oliver Ye, Anthony Tafoya, Xuqian Ma, Sylvia Ratnasamy, and Anees Shaikh. 2025. Towards Accessible Model-Free Verification. In Proceedings of the 24th ACM Workshop on Hot Topics in Networks (UMD Campus, College Park, MD, USA) (HotNets ’25). Association for Computing Machinery, New York, NY, USA, 210–217. https://doi.org/10.1145/3772356.3772380 [21] Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu. 2026. SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification. arXiv:2604.21570 [cs.SE] https://arxiv.org/abs/2604.21570 [22] William M. McKeeman. 1998. Differential Testing for Software. Digit. Tech. J. 10 (1998), 100–107. https://api.semanticscholar.org/CorpusID: 14018070 [23] Rajdeep Mondal, Rathin Singha, Todd Millstein, George Varghese, Ryan Beckett, and Siva Kesava Reddy Kakarla. 2026. Eywa: Automating Model-Based Testing using LLMs. In 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI 26). USENIX Association, Renton, WA, 777–800. https://www.usenix.org/conference/ nsdi26/presentation/mondal [24] Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. 2025. AlphaEvolve: A coding agent for scientific and algorithmic discovery. arXiv:2506.13131 [cs.AI] https://arxiv.org/abs/2506.13131 [25] Pedro Orvalho, Mikoláš Janota, and Vasco M. Manquinho. 2025. Counterexample guided program repair using zero-shot learning and MaxSAT-based fault localization. In Proceedings of the ThirtyNinth AAAI Conference on Artificial Intelligence and Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence and Fifteenth Symposium on Educational Advances in Artificial Intelligence (AAAI’25/IAAI’25/EAAI’25). AAAI Press, Article 73, 9 pages. https://doi.org/10.1609/aaai.v39i1.32046 [26] Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. 2023. Mathematical discoveries from program search with large language models. Nature (2023). https: //doi.org/10.1038/s41586-023-06924-6 [27] Tibor Schneider, Roland Schmid, Stefano Vissicchio, and Laurent Vanbever. 2023. Taming the transient while reconfiguring BGP. In Proceedings of the ACM SIGCOMM 2023 Conference (New York, NY, USA) (ACM SIGCOMM ’23). Association for Computing Machinery, New York, NY, USA, 77–93. https://doi.org/10.1145/3603269.3604855 [28] Tibor Schneider, Stefano Vissicchio, and Laurent Vanbever. 2025. Verifying maximum link loads in a changing world. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25). USENIX Association, Philadelphia, PA, 1269–1287. https://www. usenix.org/conference/nsdi25/presentation/schneider [29] Armando Solar-Lezama. 2008. Program synthesis by sketching. Ph. D. Dissertation. USA. Advisor(s) Bodik, Rastislav. [30] Alan Tang, Siva Kesava Reddy Kakarla, Ryan Beckett, Ennan Zhai, Matt Brown, Todd Millstein, Yuval Tamir, and George Varghese. 2021. Campion: debugging router configuration differences. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference (Virtual Event, USA) 7

Ioannis Protogeros, Tibor Schneider, and Laurent Vanbever (SIGCOMM ’21). Association for Computing Machinery, New York, NY, USA, 748–761. https://doi.org/10.1145/3452296.3472925 [31] Hongshu Wang, Xinyue Zuo, Yuhan Sun, Qin Li, Yamine Ait Ameur, and Jin Song Dong. 2026. Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair. arXiv:2605.17475 [cs.SE] [32] Xieyang Xu, Weixin Deng, Ryan Beckett, Ratul Mahajan, and David Walker. 2023. Test Coverage for Network Configurations. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23). USENIX Association, Boston, MA, 1717–1732. https://www. usenix.org/conference/nsdi23/presentation/xu [33] Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. 2020. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols

for Computer Communication (Virtual Event, USA) (SIGCOMM ’20). Association for Computing Machinery, New York, NY, USA, 599–614. https://doi.org/10.1145/3387514.3406217 [34] Yifei Yuan, Fangdan Ye, Yifan Li, Jingkai Zhang, Mengqi Liu, Yuyang Sang, Ruizhen Yang, Duncheng She, Zhiqing Ye, Tianchen Guo, Xiaobo Zhu, Xinji Tang, Li Jia, Zhongyu Guan, Lingpeng Su, Ci Wang, Ruiyang Feng, Shuo Wu, Zhonghui Xie, Cheng Jin, Peng Zhang, Qing Ma, Xianlong Zeng, Dennis Cai, and Ennan Zhai. 2025. New Evolution of Hoyan: Enhancing Scalability, Usability, and Accuracy for Alibaba’s Global WAN Verification. In Proceedings of the ACM SIGCOMM 2025 Conference (São Francisco Convent, Coimbra, Portugal) (SIGCOMM ’25). Association for Computing Machinery, New York, NY, USA, 809–825. https://doi.org/10.1145/3718958.3754343 [35] Yajie Zhou, Ao Li, Ashwin Silla, Zaoxing Liu, and Vyas Sekar. 2026. AIChilles: Automatically Uncovering Hidden Weaknesses in AIEvolved Systems. arXiv:2606.15834 [cs.AI] https://arxiv.org/abs/ 2606.15834

8

Related documents

• Fitness landscape analysis for the differential evolution algorithm#637735
• Exact Algorithms for Network Fortification and Design Problems under Stochastic Interdiction#244652
• Improving Network Anomaly Detection via Choquet-Integral-Based Feature Aggregation#381701
• Combating web-based fake profiles using optimized LightGBM: an ensemble learning approach using OSEMN framework#390111
• Benchmarking Terminology for Network Interconnection Devices#133550