Paper deep dive
Self-evolving network verifiers
Ioannis Protogeros, Tibor Schneider, Laurent Vanbever
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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 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.
Tags
Links
- Source: https://arxiv.org/abs/2608.11340v1
- Canonical: https://arxiv.org/abs/2608.11340v1
Trouble viewing inline? Open PDF directly ā
Full Text
40,617 characters extracted from source content.
Expand or collapse full text
Self-evolving network verifiers Ioannis Protogeros Affiliation: ETH ZĆ¼rich, ZĆ¼rich , Switzerland email: iprotogeros@ethz.ch , Tibor Schneider Affiliation: ETH ZĆ¼rich, ZĆ¼rich , Switzerland email: sctibor@ethz.ch and Laurent Vanbever Affiliation: ETH ZĆ¼rich, ZĆ¼rich , Switzerland email: lvanbever@ethz.ch 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 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. 1. Introduction ā°ECC: configuration space ā°E: environment spacecontrol-plane verificationall environments withina fixed configuration spaceā ā ā ā ā ā ā ā ā ā ā configuration,one environment at a timeā ā ā ā ā ā ā -evolvingspace grown throughoracle-checked scenarios Figure 1. A self-evolving verifier keeps the symbolic modelās guarantees and grows their coverage, guided by ground-truth observations. 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. 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 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 (31; 25; 23; 21)). 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 end-to-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. Verifier VScenarios (c,e)\(c,e)\config ā āā°EConfigurationset CEnvironmentset ā°ECoding AgentTest GeneratorEvolvingverifier VOracle ODifferential checkāā#ā”?RāTRT^\#\; ?ā”\;RTas two SMT queries (Ā§2.2)Extendedverifier +V^+extendssymbolic routing stateāā#ā(c,e)RT^\#(c,e)RāTā(c,e)RT(c,e)concrete routing stateall tests passā§ no more tests neededcounterexample(c,e)(c,e)tests and reportlatest repair (diff)more tests needed?ā add scenarios cā²,eā²\c ,e \++SeedsSelf-evolving loop 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. 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 (c,e)(c,e): 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 (14; 13)). 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 c and environment e: 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 e, 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 r each route in the routing table calculated by the Oracle RāT=ā”(c,e)RT=O(c,e), and r#r^\# its respective symbolic route under the SMT model, then that query would be eā§(ārāRāTr=r#)ā(should be sat)e ( _rā RTr=r^\# ) (should be sat) Here r=r#r=r^\# asserts, for a concrete route r 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. eā§(ārāRāTrā r#)ā(should be unsat)e ( _rā RTr =r^\# ) (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 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. 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 (c,e)(c,e) 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^+. 2.4. 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 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, hand-written encodings do not come with proofs either; they are validated with finite test suites, expert review, and hand-maintained 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. 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, (i) BGP route reflection (RFC 4456), including cluster lists, originator IDs, and their effect on best-path selection; and (i) 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 (i), and emulated FRRouting instances (via containerlab) for (i), 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. OSPF areas Route refl. L3VPN Coding Agent model Opus Sonnet Opus Sonnet Opus Sonnet Tests (seedā ) 316ā 544 316ā 648 484ā 600 484ā 600 508ā 596 508ā 582 Rounds (failing) 7 (3) 9 (1) 5 (1) 4 (0) 13 (3) 11 (2) Agent steps 95 91 200 173 218 254 Total cost ($) 41.8 35.8 30.1 18.7 37.2 25.0 Lines added 288 275 85 152 1162 1060 Final passing tests 544/544 648/648 600/600 600/600 596/596 582/582 Table 1. Every run converged to full agreement with its oracle on an implementation-aware testing suite. 3.1. What the agents modelled Figure 3 distills each converged encoding into the rules the agent effectively added, as faithful abridgements of the agentsā Rust/Z3 code. 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. Route reflection (Fig. 3i). 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. L3VPN over EVPN (Fig. 3i). 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). (i) OSPF areas define per-area distances daā(u,v)d_a(u,v): symbolic shortest paths over the area-a links that are up in the environment define Dā”(s,t)=minxāABRā”(as)yāABRā”(at)ā”dasā(s,x)+d0ā(x,y)+datā(y,t)D(s,t)\;=\; _ subarraycx\,ā\,ABR(a_s)\\ y\,ā\,ABR(a_t) subarray\;d_a_s(s,x)+d_0(x,y)+d_a_t(y,t) āŖ Despite leading to the exact same result, Opus considered the min over a much vaster space (Ā§3.3) assert each path segment is reachable within its area assert an intra-area route, when one exists, beats every inter-area route, regardless of cost (i) Route reflection define per-route attributes: cluster list CL, originator ID OID define āā”(r)::CL (r)\,::\,CL ā³ reflector r prepends its cluster ID define āsenderOID if unset assert router t admits a route iff ā tā§cāiādā(t)āOIDā t\, \,cid(t) ā³ loop rejection define lexicographic minimization along ā³ best-path selection āÆā»IGP costā»||ā»peer IDĀ·s\, \,IGP cost\, \,|CL|\, \,OID\, \,peer ID (i) L3VPN over EVPN given routers R, weighted core links L, EVPN sessions E, VRF attachments, originated prefixes O define dā”(u,v)d(u,v): shortest paths after deleting failed nodes and links define ā”(u,v)ā(u,v)āEā§both upā§dā”(u,v)<āact(u,v)\, \,(u,v)ā E\, \,both up\, \,d(u,v)<ā ā³ EVPN session liveness define oāto t: RFC 4456 reflection reachability over act ā³ overlay R define ā”(v)=rt(v)= ASN:VNI if auto, ā”(v)=rd(v)= routerID:vrfID if auto ā³ route target / distinguisher define a type-5 route is āØā”(o),p,ā”(o),ā”(o)ā© (o),\,p,\,RT(o),\,A(o) ā³ RD keys identity define āŗ=(Ā¬ā,LP,|ASpath|,origin,MED,eBGPāŗiBGP, \;=\; ( ,\,LP,\,|ASpath|,\,origin,\,MED,\,eBGP iBGP, OPENIGP cost,router ID)IGP cost,\,router ID ) ā³ full decision process define ā”(r,,p)=mināŗā”o:ā”(o)=ā§dā”(r,o)<āā§oārebest(r,rd,p)= _ \,\\,o\,:\,rd(o)=rd\, \,d(r,o)<ā\, \,o r\,\ ā³ EVPN RIB: selection per (RD, prefix), not across RDs define (r,v,p)=(r,,p):imp(r,v)ā(o)cand(r,v,p)=\\,ebest(r,rd,p)\,:\,rt^imp(r,v) (o) ā§(o)ā (v) \;\,rd(o) (v)\,\ ā³ leak: import filter + self-RD rejection define ā”(r,v,p)=mināŗā”(r,v,p)best(r,v,p)= _ \,cand(r,v,p) ā³ tenant v4 RIB: cross-RD competition resolved here Figure 3. The two agents converged to semantically equivalent encodings. 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 notion of coverage over a targeted scenario space, is, we argue, a core open problem for self-evolving verifiers (Ā§4). passingĆfailing (count)converged 0033669920020040040060060010048544/544tests passed (a) OSPF areas ā Ā· Opus 0033669910020648/648 (b) OSPF areas ā Ā· Sonnet 00336699450450525525600600512600/600roundtests passed (c) Route reflection ā Ā· Opus 0033669951600/600round (d) Route reflection ā Ā· Sonnet Figure 4. An evolved verifier that passes all tests in a single round might still fail on different inputs. 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. 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. 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. Two more rounds add no failing test cases. Converged: 544/544. Figure 5. The Test Generator proposes adversarial scenarios until it cannot invent further ones. 3.3. 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 single-link 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 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Ć2Ć faster on the same proof, so even within verifiers with similar network models and the same end results, performance may vary significantly. 4. 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 ground-truth behaviour, and such scenarios are sparse: validating the order of a decision process at step k requires routes with equal attributes on all previous steps, as in the route-reflection 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? 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 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. 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 Arashloo et al. (2023) M. T. Arashloo, R. Beckett, and R. Agarwal Formal methods for network performance analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), Boston, MA, p. 645ā661. External Links: ISBN 978-1-939133-33-5, Link Cited by: Ā§4. Bates et al. (2006) T. Bates, E. Chen, and R. Chandra BGP route reflection: an alternative to full mesh internal BGP (IBGP). RFC Editor. Note: RFC 4456 External Links: Document, Link Cited by: Ā§1. Batfish Project (2025) Batfish Project Batfish v2025.07.07, BgpRib.java. Note: https://github.com/batfish/batfish/blob/v2025.07.07/projects/batfish/src/main/java/org/batfish/dataplane/rib/BgpRib.java Cited by: Ā§3.1. Beckett et al. (2017) R. Beckett, A. Gupta, R. Mahajan, and D. Walker A general approach to network configuration verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM ā17), p. 155ā168. External Links: Document Cited by: Ā§1, Ā§1. Beckett et al. (2018) R. Beckett, A. Gupta, R. Mahajan, and D. Walker Control plane compression. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM ā18, New York, NY, USA, p. 476ā489. External Links: ISBN 9781450355674, Link, Document Cited by: Ā§4. Beckett et al. (2020) R. Beckett, A. Gupta, R. Mahajan, and D. Walker Abstract interpretation of distributed network control planes. Proceedings of the ACM on Programming Languages 4 (POPL). Cited by: Ā§1, Ā§1. Birkner et al. (2021) R. Birkner, T. Brodmann, P. Tsankov, L. Vanbever, and M. Vechev Metha: network verifiers need to be correct too!. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21), p. 99ā113. External Links: ISBN 978-1-939133-21-2, Link Cited by: Ā§1, Ā§2.4. Brown et al. (2023) M. Brown, A. Fogel, D. Halperin, V. Heorhiadi, R. Mahajan, and T. Millstein Lessons from the evolution of the batfish configuration analysis tool. In Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM ā23, New York, NY, USA, p. 122ā135. External Links: ISBN 9798400702365, Link, Document Cited by: Ā§1, Ā§1, Ā§2.4. Chockler et al. (2003) H. Chockler, O. Kupferman, and M. Vardi Coverage metrics for formal verification. Vol. 8, p. 111ā125. External Links: ISBN 978-3-540-20363-6, Document Cited by: Ā§4. de Moura and BjĆørner (2008) L. de Moura and N. BjĆørner Z3: an efficient smt solver. Vol. 4963, p. 337ā340. External Links: ISBN 978-3-540-78799-0, Document Cited by: Ā§3. Fogel et al. (2015) A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein A general approach to network configuration analysis. In Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation, NSDIā15, USA, p. 469ā483. External Links: ISBN 9781931971218 Cited by: Ā§3. FRRouting Project (2026) FRRouting Project FRRouting 10.6.1, bgpd/bgp_route.c, function bgp_path_info_cmp. Note: https://github.com/FRRouting/frr/blob/frr-10.6.1/bgpd/bgp_route.c Cited by: Ā§1, Ā§3.1. Gao and Rexford (2001) L. Gao and J. Rexford Stable internet routing without global coordination. IEEE/ACM Transactions on Networking 9 (6), p. 681ā692. External Links: Document Cited by: Ā§2.1. Griffin et al. (2002) T.G. Griffin, F.B. Shepherd, and G. Wilfong The stable paths problem and interdomain routing. IEEE/ACM Transactions on Networking 10 (2), p. 232ā243. External Links: Document Cited by: Ā§2.1. Gulwani et al. (2017) S. Gulwani, O. Polozov, and R. Singh Program synthesis. Foundations and TrendsĀ® in Programming Languages 4, p. 1ā119. External Links: Document Cited by: Ā§1. Hoskote et al. (1999) Y. Hoskote, T. Kam, P. Ho, and X. Zhao Coverage estimation for symbolic model checking. In Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), Vol. , p. 300ā305. External Links: Document Cited by: Ā§4. Jha and Seshia (2016) S. Jha and S. A. Seshia A theory of formal synthesis via inductive learning. External Links: 1505.03953, Link Cited by: Ā§2.3. Kazemian et al. (2012) P. Kazemian, G. Varghese, and N. McKeown Header space analysis: static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), San Jose, CA, p. 113ā126. External Links: ISBN 978-931971-92-8, Link Cited by: Ā§1. Khurshid et al. (2013) A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. Godfrey VeriFlow: verifying Network-Wide invariants in real time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), Lombard, IL, p. 15ā27. External Links: ISBN 978-1-931971-00-3, Link Cited by: Ā§1. Krentsel et al. (2025) A. Krentsel, O. Ye, A. Tafoya, X. Ma, S. Ratnasamy, and A. Shaikh Towards accessible model-free verification. In Proceedings of the 24th ACM Workshop on Hot Topics in Networks, HotNets ā25, New York, NY, USA, p. 210ā217. External Links: ISBN 9798400722806, Link, Document Cited by: Ā§1, Ā§1, Ā§2.4, Ā§4. Ma et al. (2026) L. Ma, S. Liu, Y. Li, Q. Wu, H. Wang, and L. Bu SpecSyn: llm-based synthesis and refinement of formal specifications for real-world program verification. External Links: 2604.21570, Link Cited by: Ā§1. McKeeman (1998) W. M. McKeeman Differential testing for software. Digit. Tech. J. 10, p. 100ā107. External Links: Link Cited by: Ā§2.4. Mondal et al. (2026) R. Mondal, R. Singha, T. Millstein, G. Varghese, R. Beckett, and S. K. R. Kakarla Eywa: automating Model-Based testing using LLMs. In 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI 26), Renton, WA, p. 777ā800. External Links: ISBN 978-1-939133-54-0, Link Cited by: Ā§1. Novikov et al. (2025) A. Novikov, N. VÅ©, M. Eisenberger, E. Dupont, P. Huang, A. Z. Wagner, S. Shirobokov, B. Kozlovskii, F. J. R. Ruiz, A. Mehrabian, M. P. Kumar, A. See, S. Chaudhuri, G. Holland, A. Davies, S. Nowozin, P. Kohli, and M. Balog AlphaEvolve: a coding agent for scientific and algorithmic discovery. External Links: 2506.13131, Link Cited by: Ā§4. Orvalho et al. (2025) P. Orvalho, M. Janota, and V. M. Manquinho Counterexample guided program repair using zero-shot learning and maxsat-based fault localization. In Proceedings of the Thirty-Ninth 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. External Links: ISBN 978-1-57735-897-8, Link, Document Cited by: Ā§1, Ā§2.3. Romera-Paredes et al. (2023) B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont, F. J. R. Ruiz, J. Ellenberg, P. Wang, O. Fawzi, P. Kohli, and A. Fawzi Mathematical discoveries from program search with large language models. Nature. External Links: Document Cited by: Ā§4. Schneider et al. (2023) T. Schneider, R. Schmid, S. Vissicchio, and L. Vanbever Taming the transient while reconfiguring BGP. In Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM ā23, New York, NY, USA, p. 77ā93. External Links: Link, Document, ISBN 9798400702365 Cited by: Ā§4. Schneider et al. (2025) T. Schneider, S. Vissicchio, and L. Vanbever Verifying maximum link loads in a changing world. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25), Philadelphia, PA, p. 1269ā1287. External Links: ISBN 978-1-939133-46-5, Link Cited by: Ā§4. Solar-Lezama (2008) A. Solar-Lezama Program synthesis by sketching. Ph.D. Thesis, University of California at Berkeley, USA. External Links: ISBN 9781109097450 Cited by: Ā§2.3. Tang et al. (2021) A. Tang, S. K. R. Kakarla, R. Beckett, E. Zhai, M. Brown, T. Millstein, Y. Tamir, and G. Varghese Campion: debugging router configuration differences. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference, SIGCOMM ā21, New York, NY, USA, p. 748ā761. External Links: ISBN 9781450383837, Link, Document Cited by: Ā§1. Wang et al. (2026) H. Wang, X. Zuo, Y. Sun, Q. Li, Y. Ait Ameur, and J. S. Dong Event-B agent: towards LLM agent for formal model synthesis and repair. External Links: 2605.17475 Cited by: Ā§1. Xu et al. (2023) X. Xu, W. Deng, R. Beckett, R. Mahajan, and D. Walker Test coverage for network configurations. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), Boston, MA, p. 1717ā1732. External Links: ISBN 978-1-939133-33-5, Link Cited by: Ā§4. Ye et al. (2020) F. Ye, D. Yu, E. Zhai, H. H. Liu, B. Tian, Q. Ye, C. Wang, X. Wu, T. Guo, C. Jin, D. She, Q. Ma, B. Cheng, H. Xu, M. Zhang, Z. Wang, and R. Fonseca 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, SIGCOMM ā20, New York, NY, USA, p. 599ā614. External Links: ISBN 9781450379557, Link, Document Cited by: Ā§1. Yuan et al. (2025) Y. Yuan, F. Ye, Y. Li, J. Zhang, M. Liu, Y. Sang, R. Yang, D. She, Z. Ye, T. Guo, X. Zhu, X. Tang, L. Jia, Z. Guan, L. Su, C. Wang, R. Feng, S. Wu, Z. Xie, C. Jin, P. Zhang, Q. Ma, X. Zeng, D. Cai, and E. Zhai New evolution of hoyan: enhancing scalability, usability, and accuracy for alibabaās global wan verification. In Proceedings of the ACM SIGCOMM 2025 Conference, SIGCOMM ā25, New York, NY, USA, p. 809ā825. External Links: ISBN 9798400715242, Link, Document Cited by: Ā§2.4, Ā§4. Zhou et al. (2026) Y. Zhou, A. Li, A. Silla, Z. Liu, and V. Sekar AIChilles: automatically uncovering hidden weaknesses in ai-evolved systems. External Links: 2606.15834, Link Cited by: Ā§4.