# Self-evolving network verifiers

arXiv: https://arxiv.org/abs/2608.11340 · HTML: https://mlsanity.com/paper/2608.11340/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 34 references that are in the map.
- First posted on arXiv 11 Aug 2026.

## Builds on (most cited first, 5 of 5)

- [A Theory of Formal Synthesis via Inductive Learning](https://mlsanity.com/paper/1505.03953/) (2015)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Control Plane Compression](https://mlsanity.com/paper/1806.08744/) (2018)
- [Eywa: Automating Model Based Testing using LLMs](https://mlsanity.com/paper/2312.06875/) (2023)
- [AIChilles: Automatically Uncovering Hidden Weaknesses in AI-Evolved Systems](https://mlsanity.com/paper/2606.15834/) (2026)

## Abstract (arXiv)

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.