💻 computer science

Self-evolving network verifiers

This paper proposes "Self-evolving network verifiers," a system that autonomously learns and refines symbolic network models by iteratively comparing a coding agent's proposals against ground-truth router behavior, thereby eliminating the need for manual, error-prone model maintenance and enabling verification of complex, vendor-specific network features.

Original authors: Ioannis Protogeros, Tibor Schneider, Laurent Vanbever

Published 2026-08-13

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Ioannis Protogeros, Tibor Schneider, Laurent Vanbever

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine the internet as a giant, invisible city made entirely of roads, traffic lights, and delivery trucks. In this city, the "traffic lights" are actually complex computer programs running on routers, deciding exactly where every piece of data should go. If these programs make a mistake, the whole city can gridlock, causing the internet to crash. For years, engineers have tried to build "super-traffic controllers"—software tools that can predict every possible traffic jam before it happens, even if a road suddenly disappears or a new rule is added. These tools are like crystal balls that can see the future of the network.

However, there's a catch. To use these crystal balls, you have to first teach them the rules of the road. But the rules aren't written in a single, perfect book. Instead, they are scattered across thousands of pages of technical manuals, and different companies (like the makers of Cisco or Juniper routers) sometimes interpret the rules slightly differently. It's like trying to teach a robot to drive in a city where every street sign is written in a different dialect, and the signs change every time the city updates its software. Keeping the robot's map up-to-date is a never-ending, exhausting job for human experts. If the map is even a little wrong, the crystal ball gives a false prediction, and the network remains vulnerable to crashes.

This is where a new idea from researchers at ETH Zürich comes in. They propose that instead of having a human expert painstakingly draw the map, we should let the map draw itself. They built a system where a "robot coder" (an AI) watches a real router (or a perfect simulation of one) and learns the rules by watching what it actually does. If the robot coder's map says "turn left," but the real router turns right, the robot coder fixes its map immediately. It's like a student learning to drive by sitting in the passenger seat, watching the instructor, and correcting their own mental map every time they get a direction wrong.

The researchers tested this idea by giving their system three complex driving rules it didn't know: how to handle different neighborhoods (OSPF areas), how to manage traffic through a central hub (BGP route reflection), and how to deliver packages across different virtual cities (L3VPN over EVPN). The system didn't just guess; it used a "ground truth" simulator as a trusted teacher. When the AI's model disagreed with the simulator, the simulator provided a "counterexample"—a specific scenario where the AI was wrong. The AI then rewrote its own code to fix that specific mistake.

The results were surprisingly successful. In just a few rounds of this "guess-and-check" loop, the system taught itself all three complex features. It even discovered that some routers follow a slightly different order of operations than the official rulebooks say, catching vendor-specific quirks that human experts often miss. The whole process cost only about $30 to $40 in computer time per feature and took a few hundred steps for the AI to figure out.

However, the paper is careful to note that this isn't a magic wand that solves everything instantly. The system is great at learning what it has been tested on, but it can't guarantee it will never make a mistake in a situation it hasn't seen yet. It's like a student who has aced every practice test but might still be surprised by a trick question on the final exam. The researchers suggest that the real challenge now isn't writing the code, but building better "test generators" to keep throwing tricky scenarios at the AI to ensure it's truly ready for the real world. They also found that while the AI could learn the rules, it sometimes wrote code that was correct but very slow, requiring a second round of "optimization" to make it fast enough for real use.

In short, this paper suggests a new way to build network safety tools: stop trying to manually write the rulebook for every possible router, and instead let an AI learn the rules by watching the routers work, correcting its mistakes with the help of a trusted simulator. It's a shift from "human experts drawing the map" to "AI learning to drive by watching the road," promising to make the internet safer and easier to manage, provided we keep testing the AI's driving skills rigorously.

Technical Summary: Self-Evolving Network Verifiers

Problem Statement

Network verification tools are theoretically capable of reasoning about correctness across vast spaces of routing inputs and link failures. However, their practical adoption is hindered by the reliance on hand-crafted control-plane models. These models must be manually encoded by experts to represent specific protocols and vendor implementations. This process is Sisyphean: vendor implementations often deviate from RFCs, behavior shifts with software releases, and undocumented semantics are common. Consequently, existing verifiers support only a subset of features actually deployed, leaving many networks unverified.

While "model-free" approaches (running configurations on emulated networks) avoid the encoding burden, they sacrifice the ability to reason about all possible environments (e.g., all link failures) simultaneously, as enumerating every possible data plane is computationally intractable. The core problem is not the reliance on models, but the manual labor required to create and maintain them.

Methodology

The paper proposes a self-evolving verifier that automatically adapts its symbolic model to faithfully capture actual network behavior. The system operates on the premise that the router software itself is the only unambiguous source of truth. The methodology employs a Counterexample-Guided Inductive Synthesis (CEGIS) loop, augmented by Large Language Models (LLMs) and network emulation.

The loop consists of three primary components:

The Oracle ( $O$ ): A trusted source of ground truth, such as a network emulator (e.g., containerlab with FRRouting) or a high-fidelity simulator (e.g., Batfish). Given a configuration ( $c$ ) and a concrete environment ( $e$ ), the Oracle returns the converged routing state ($RT$).
The Symbolic Verifier ( $V$ ): An SMT-based model that attempts to reason about routing states across all environments.
The Agents:
- Coding Agent: An LLM tasked with modifying the verifier's symbolic encoding (e.g., Rust/Z3 code) to resolve discrepancies.
- Test Generator: An LLM that analyzes the current code and test suite to propose new, adversarial scenarios ( $c', e'$ ) to stress-test the model.

The Differential Testing Loop

The system validates the model through differential testing against the Oracle for specific scenarios:

Soundness Check: Does the SMT model reject a routing state observed in the Oracle? The system queries if the Oracle's state is possible under the SMT constraints. If the Oracle's state is valid but the SMT model says "unsat," the model is too restrictive.
Completeness Check: Does the SMT model accept a routing state that the Oracle does not produce? The system queries if the SMT model can generate a state different from the Oracle's. If "sat," the model admits spurious states.

The Evolution Process:

Seed: The corpus is seeded with initial scenarios.
Test: The system runs differential tests. Any disagreement between the Oracle and the Verifier generates a counterexample.
Repair: The Coding Agent receives the counterexample, the failing query, and the Oracle's ground truth. It edits the symbolic encoding to fix the specific discrepancy.
Regression Check: The entire corpus is re-run to ensure the fix does not break previously passing scenarios.
Expansion: The Test Generator attempts to invent new scenarios that the current model might fail. If new counterexamples are found, the loop repeats.
Termination: The loop ends when all tests pass and the Test Generator cannot produce further adversarial scenarios.

Key Contributions

Vision of Automatic Model Evolution: The paper argues for shifting the burden from writing verification systems to systematically testing them. It proposes that symbolic models should evolve automatically to match the "executable ground truth" of router software.
Implementation of the Loop: A concrete implementation using an LLM-based coding agent and a test generator to repair a 3,000-line Rust SMT verifier.
Demonstration of Feature Learning: The system successfully taught the verifier three complex features it did not originally support:
- OSPF Areas: Handling inter-area distance calculations and partitioning.
- BGP Route Reflection: Including cluster lists and originator IDs, and adapting to vendor-specific deviations from RFC 4456 (e.g., FRR's specific decision order).
- L3VPN over EVPN: Modeling complex decision processes and private route preferences not fully specified in standards.
Performance Optimization: The system demonstrated the ability to optimize for performance (computational tractability) alongside correctness. When instructed to improve scaling, the agent independently reinvented optimizations (e.g., restricting path searches to Area Border Routers) that reduced query times from intractable (>20 mins) to sub-second.

Results

The prototype was evaluated on a 3,000-line SMT-based verifier.

Convergence: All successful runs converged to full agreement with their respective oracles on adversarially grown test suites.
Cost: The process cost tens of dollars per feature (approx. $18–$ 42) and required ~100–250 agent steps per feature.
Model Quality: The agents converged on semantically equivalent encodings for the same features, even when using different LLMs (Opus vs. Sonnet).
Vendor Specificity: The agents successfully learned vendor-specific behaviors that deviated from RFCs (e.g., FRR's route reflection logic) solely through counterexamples, without explicit human instruction on the deviation.
Performance Variance: While different agents produced correct models, their performance varied significantly (orders of magnitude). One agent's encoding was intractable at small scales, while another's was efficient, highlighting that correctness does not guarantee performance.

Significance and Claims

The paper claims that this approach shifts the hard problem of network verification from "writing verification systems" to "systematically testing them."

Accessibility: By automating model growth, verification becomes accessible to networks that currently lack the expert labor to maintain hand-crafted models.
Fidelity: The approach ensures models reflect actual vendor behavior rather than idealized RFC specifications.
Research Agenda: The authors identify critical open questions for this paradigm:
- Testing Adequacy: How to ensure the "Test Generator" has exhausted the search space and that no counterexamples remain.
- Performance Optimization: How to systematically steer agents toward efficient encodings, not just correct ones.
- Scope of Properties: Extending the loop beyond static routing states to transient states and performance metrics (e.g., link loads).
- Universal vs. Ad-hoc: Whether the community should maintain a single universal verifier or allow per-network verifiers that evolve with specific configurations. The results suggest a hybrid approach where a community corpus of adversarial scenarios could validate ad-hoc verifiers.

The paper concludes that while a passing run does not constitute a formal proof of correctness across all environments, it provides a level of confidence comparable to (or exceeding) current hand-written models, which are also validated via finite test suites and expert review. The system represents a step toward making network verification robust, scalable, and adaptable to the reality of modern network deployments.