Axiom: a logic programming language to express and enforce network designs

arXiv:2610.36748v1 [cs.NI] 27 Oct 2026

Axiom: a logic programming language to express and enforce network designs Tibor Schneider

Laurent Vanbever

ETH Zurich Zurich, Switzerland

ETH Zurich Zurich, Switzerland

ABSTRACT

and support every possible implementation. For instance, to reach external destinations, a network can propagate their routes over iBGP in various topologies, redistribute them into OSPF or IS-IS, or mix both with static routes on top. A network deploys one of them, yet verifiers must accept them all: They must (i) model all protocols plus their interactions, (ii) build the full symbolic network state before checking, and (iii) cannot blame any command, as each could be intended. We therefore argue that operators should state not only the intended behavior, but also how they plan to implement it: the network’s design. In the example above, the design would not require reachability, but that the iBGP sessions form a route-reflection topology. Operators already make these design decisions, e.g., OSPF within regions and BGP in between, a dedicated VRF to isolate management traffic, and L3VPNs connecting customer sites. A configuration implements a design if each of its decisions hold; checking this (i) requires modeling only the commands the design uses, (ii) amounts to a fast check on the configuration text, and (iii) points directly at the invalid commands, like those configuring invalid iBGP sessions in the example above. Hyperscalers seem to agree: their custom management systems [30, 35, 50] make their design explicit, and either check configuration changes against it or generate them from the design. But these systems are tailored to their own design and tightly integrated in their tooling; they would not fit other networks even if they were open-sourced. The vast majority of networks lack the resources to engineer such a solution and are left with no tool to capture their design: Existing tools either check local configuration properties [8] or analyze the behavior produced by a configuration [10, 14]. Although operators can script custom analyses over tools such as Batfish, those scripts are written against configurations or network state [40], not against an explicit representation of the network’s design. We instead propose Axiom, a language that makes the design itself a first-class citizen that can be checked. It is built around two goals: The first is to be flexible: every network’s design is different, so operators must be able to state their own decisions rather than pick from predefined checks.

Human errors remain the leading cause of network outages. To prevent them researchers propose general verifiers that analyze the network behavior. Yet, their (symbolic) models struggle to accurately reflect network devices, they fail to scale to large networks, and report misbehavior, not what configuration line caused it. We attribute all three challenges to specifications that describe the intended behavior but not how operators intend to achieve it—the network’s design: which protocols to run and how to combine them. We present Axiom, a language for expressing network designs, and a checker that finds every violation and the responsible commands. Operators state their design decision as rules over configuration commands. Axiom then compiles them into a single Datalog program that checks the entire network directly on its configurations, not on the state they produce. Our prototype checks a 754-router network within seconds. Ultimately, a design enforced on every keystroke could give network operators the integrated development environment that programmers have long enjoyed.

1

INTRODUCTION

Network misconfigurations keep causing large-scale and long-lasting outages [23, 39, 45]. Decades of research have answered with network verifiers that promise to catch bugs offline, before they reach production by comparing the configuration’s behavior against the operators’ intent. Yet, only a small fraction of production networks deploy them [28], and the reasons are well known in the literature: Verifiers (i) need high-fidelity models of deployed devices [10, 28, 41], (ii) struggle to scale to large networks [29, 46, 53, 55], and (iii) report misbehavior, but help little in debugging [46, 54]. We agree with all three, but see them as symptoms of a single root cause: verifiers assume nothing about how operators intend to implement the behavior. Seeing only what is configured, not what is intended, they must be generic

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License. 1

Tibor Schneider and Laurent Vanbever

1 rel Addr(device: String, iface: String, addr: IpAddr);

Axiom therefore builds on Datalog: operators write design decisions as rules, and recursion lets those rules span the entire network rather than a single device. The second is to operate directly on configurations, not on a model derived from them. A templating layer matches configuration commands and exposes their parameters to the design rules, linking each derived fact to the command it came from. Thus, Axiom is tied to no vendor or device. The same language can capture router configurations, and those from applications like DNS or web servers, letting operators express dependencies between applications and the network. We find that writing a design is little work that pays off in fast checks and localized feedback: 140 lines suffice to check a 4-million-line configuration of a 754-node network, and Axiom does so in five seconds while locating the commands that violate the design. Axiom’s benefits are not for free. With verifiers, the cost is complex models, slow checks, and vague errors; with Axiom, it is effort: operators must write the design and ensure it is correct. We argue that both efforts are smaller than they appear. Writing a design does involve modeling, but only proportionally: operators write templates only for the commands they use and rules only for the decisions they make, never describing how the network computes its forwarding state. Further, they need not start from scratch: just as existing tools mine behavioral specifications [9], templates [24], or device-local contracts [8] from configurations, future tools could mine the design a configuration already implements. True to its name, Axiom takes the design as an axiom: any configuration that implements it is assumed correct. If the design is incorrect, so is every conclusion built on it. Yet, this assumption is nothing new, as operators today already trust their design. That trust is implicit, and since only a few networks run a verifier, it goes entirely unchecked. Axiom instead makes it explicit and at least guarantees that the configuration correctly implements the design. Beyond checking, an explicit design opens opportunities for the tools that manage configurations. A check that finishes in seconds and points at the offending command can run mid-edit and give network engineering the integrated development environment (IDE) that programmers have long enjoyed. Further, a violated rule carries more than a location: its negative provenance [59] explains which facts are missing for the design to hold, the building blocks for automatically suggesting fixes. The same feedback turns the checker into an oracle for LLMs that guarantees their edits preserve the design, not just the behavior [36]. Axiom could even constrain the generation directly like type systems already do [38]. Ultimately, provenance and constrained generation aim at the same goal: entire configurations produced and updated from the design itself, bringing the end-to-end tooling of hyperscalers to every other network.

2 rel Asn(device: String, asn: Int); 3 rel IBgpSession(device: String, neighbor: String, ip: IpAddr); 4 5 def ("interface", iface: String, "ip", "address", ip: IpNet): 6 set Addr(self, iface, ip as IpAddr); // Router <--> IP mapping 7 8 def ("router", "bgp", asn: Int) { 9 set Asn(self, asn); // Router <--> AS number mapping 10 11 12 13 14 15 16 17 18 19 20 21 }

def ("neighbor", ip: IpAddr, "remote-as", remote_asn: Int) { if asn == remote_asn { for Addr(_ as N: String, _, ip) { assert Asn(N, remote_asn): "Invalid remote-as: " ++ N; set IBgpSession(self, N, ip); } assert IBgpSession(self, _, ip): "No router has IP " ++ ip; } } for Asn(_ as N: String, asn): if N != self: assert IBgpSession(self, N, _): "Missing session with " ++ N;

22 ! Configuration of r1 23 interface eth0 24 ip address 5.0.0.1/24

27 ! configuration of r2 28 interface eth0 29 ip address 5.0.0.2/24

25 router bgp 5 30 router bgp 5 26 neighbor 5.0.0.2 remote-as 5 31 neighbor 5.0.0.1 remote-as 5

Figure 1: Axiom design to enforce an iBGP full-mesh, along with the configuration of two routers r1 and r2.

2

AXIOM BY EXAMPLE

Consider Figure 1: the design (top) checks that two routers r1 and r2 (bottom) form an iBGP full mesh. Like every Axiom design, it combines set statements to model the configuration, storing facts in a database, and assert statements that check properties over that database. Axiom then generates a single network-wide Datalog program. Local facts. Section 1 matches every interface that configures an IP address, binding the interface name and the address. It matches twice, and each executes the body with the bound values as constants: the set statement inserts a fact into the Addr relation (declared on Section 1), yielding two Datalog facts: Addr(r1, eth0, 5.0.0.1) and Addr(r2, eth0, 5.0.0.2). Section 1 stores all AS numbers in Asn the same way. iBGP sessions. Checking a BGP session requires more than the local configuration: r1 refers to its neighbor only by IP address, while that neighbor’s name and AS number live in r2’s configuration. Datalog bridges this gap: the for statement on Section 1 searches Addr for the router N owning the configured IP—a string known only once the Datalog program runs. Each statement in its body therefore compiles to Datalog joins with relation Addr over N: the set on Section 1 becomes a rule deriving the session in IBgpSession, and the assert on Section 1 a query requiring N to have the configured remote_asn. If no router owns the configured IP, no 2

Axiom : a logic programming language to express and enforce network designs

session is derived; the assertion on Section 1 catches exactly this case.

global

verifiers simulators

iBGP full mesh. IBgpSession contains all correctly configured sessions, so this check reduces to a single join with Asn: Section 1 assert that every router maintains a session with every other in its AS. Note, that each assert is a distinct failure mode: a mismatched remote-as, a neighbor IP that no router owns, and a missing session. If any fail, Axiom reports a user-defined message pointing to the offending command.

specific

generic

Axiom

Concord [8]

pre-commit

local

3

CHECKING A NETWORK DESIGN Figure 2: Axiom enables writing designs ranging from specific to generic, and covering low-level and highlevel properties.

Figure 2 relates Axiom to existing approaches along two dimensions. The x-axis shows generality: how many valid configurations a checker accepts. Verifiers and simulators are generic and (try to) accept any configuration with the intended behavior; a design accepts only those that implement it. The y-axis shows expressivity: the scope of the checked properties, from local ones on a single device’s configuration to global ones spanning the entire network. Where a checker sits on these axes determines the cost of its checks and the precision of its errors, as we show in the following.

We find that it can, again by fixing the implementation. Consider a waypoint property: traffic towards a server must traverse a firewall. A verifier must support every possible implementation, but a design fixes one. Say the network implements the waypoint with IPv6 segment routing. The property then holds if (i) the IGP is configured correctly, (ii) every border router inserts a firewall segment, and (iii) no static route overrides the IGP towards the firewall or the server— three checks directly on the configuration text. Notably, this guarantee extends to every failure in which the network stays connected, without any explicit failure model. Beyond correctness, a design can also enforce performance objectives. To respect a hardware limit on the forwarding table size, for example, a design may require strict filters on incoming BGP routes, a cap on routes propagated in OSPF, and a default route. Where the limits of this approach lie remains open, but we conjecture that most reachability and security properties can be expressed as a design by trading generality for expressivity.

Generality. Generic specifications need to be only stated once; they cover any configuration change, including ones that replace entire protocol stacks. However, a specification is only tenuously connected to the configuration: proving that an arbitrary configuration satisfies it is expensive, and a violation cannot be attributed to a specific configuration edit. A specific design inverts this trade-off: it is cheap to check and its errors point at concrete commands, but it rejects correct configurations that implement a different design. Crucially, Axiom can express both ends of this trade-off, as two designs for iBGP route propagation illustrate. A generic design states only the intended behavior: a route originated at any router must reach every other router. Axiom can express this through recursion on the propagation graph and an assertion that tests every router pair. Doing so, however, is expensive as our evaluation in section 5 shows, and if a session is missing, it reports that routes fail to propagate, not why. The full-mesh design of Section 2 sits at the specific end: it fixes one implementation. The checks reduce to simple joins, and a missing session can be flagged directly.

4

AXIOM

Section 2 introduced Axiom’s language by example. This section presents the machinery around it: the inputs, how configurations and designs map to Datalog, and how our prototype executes them. The main input of Axiom is a network.toml. It contains the network topology, that is, all devices, their interface names, and all connections. Axiom automatically populates some Datalog relations with this information, making it accessible from the design. Besides the topology, for every device, it lists the path to its configuration files and how to parse them, and the .ax files containing the design to check. Axiom parses each configuration into a common treelike structure. This tree is Axiom’s only assumption about its input: whether the configuration belongs to a router, a

Expressivity. Existing tools sit at the two ends of this axis: pre-commit checks and configuration contracts [8] check local properties of a single configuration, such as whether every referenced route-map exists, while verifiers and simulators check global ones over the converged routing and forwarding state. Local properties are natural to express in Axiom; the question is whether a design can capture global ones without computing that state. 3

Tibor Schneider and Laurent Vanbever

switch, or an application like a DNS server, the same design language can match it, and express dependencies across all of them. Nested def statements (Section 1) match paths in this tree, and their match types (String or IpNet) determine how the configuration values are interpreted. While Axiom unifies the configuration syntax into a tree, it does not unify the semantics; doing so would require modeling every vendor and every subtle difference between their devices. Instead, the semantics live in the design itself, which remains vendor-specific. To avoid duplication, the apply mechanism shares parts of a design across vendors.

4.1

tables. The language itself is still young: it can encode prefixlists and route-maps, but not always conveniently, and a few features are still missing entirely (discussed in Section 7).

4.2

Execution

We implement a prototype of Axiom in Rust1 . It runs in three steps: parsing all configuration and .ax files, evaluating the resulting intermediate representation (IR), and running the generated Datalog program. Configurations are parsed as specified in the network.toml. For .ax files, we specify its grammar as a PEG [16]. The remaining steps are detailed as follows: Evaluating the IR. This step matches all def blocks against the parsed configurations to generate a single Datalog program. Axiom recursively walks each configuration tree while maintaining, for every matching def block, an evaluation context that binds the matched variables and accumulates all if conditions and for queries. From this context, it generates the rules and queries that constitute the Datalog program. Two kinds of variables appear along the way: those bound to concrete configuration values are evaluated directly in the IR, while symbolic ones from for bindings (capitalized and colored red in Figure 1) are left to the Datalog engine.

Stratified Datalog with Lattices

Unlike most verifiers, Axiom relies on Datalog instead of a general-purpose solver like SMT. We do so for two reasons. First, Datalog’s cost is predictable: Operators can identify the rules that dominate execution time or memory, and improve them by reordering joins or adding guards. Second, Datalog derives all facts, not just a verdict. While this may seem wasteful, every derivation carries provenance [59] leading to configuration lines. This lets tooling explain why a design fails and what commands are responsible, or even suggest completions. Datalog also matches the shape of the problem. Protocol semantics and the topology relate configuration objects across devices (like how the BGP neighbor statement of one router relates to an IP address of another in Section 2) and a join follows such a relation. Global properties, however, must follow such relations transitively, which requires recursion. It is exactly this lack of recursion that prevents Concord’s contracts [8] from expressing global properties. Recursion alone is not enough, as designs also constrain what must be absent: an interface that is shut down, for example, disables all its configuration. Datalog only derives facts and never retracts them, so a rule may check for the absence of a tuple only once that relation is fully evaluated. Stratification orders rules to guarantee any computed fixpoint is consistent. A common operation of routers and switches is to reduce many candidates to a single best one, e.g., the longest prefix, the shortest path; an operation off-the-shelf Datalog does not support. Recent Datalog variants model such a column as a lattice [3, 32, 33] that imposes an ordering on the column’s values, and the engine keeps only the best one. A consistent fixpoint requires rules on lattices to be monotone, that is, to only grow the value; we resolve non-monotone rules with stratification. Recursion, stratification, and lattices are the ingredients needed to express every design we have written thus far, including generic ones that compute parts of the routing

Datalog engine. We implement our own Datalog engine to support lattice semantics. A lightweight motion analysis first tracks how each value evolves during the fixpoint computation: it only grows, only shrinks, remains stable, or is none of the three. A rule is monotone if its values are all stable, or if the lattice agrees with its motion, e.g., a minimum lattice accepts only stable or shrinking values. This analysis stratifies the program, akin to monotonic aggregation [43]. A simple query planner prepares table indices from the join patterns of the rules: non-lattice relations are indexed whenever a join needs it, whereas lattice relations are indexed once fully evaluated. Axiom then executes each stratum using semi-naïve evaluation [4], and checks all asserts once their referenced relations are fully evaluated. Our prototype does not yet evaluate incrementally, but the literature on incremental Datalog is extensive [20, 22, 37, 44], including for lattice semantics [51, 52]. We see an incremental engine as a promising direction, especially for checking the configuration on every keystroke.

5

EARLY RESULTS

In the following, we investigate three questions about Axiom: (i) whether its language captures designs concisely, (ii) whether its checker scales to large networks, and (iii) how specific designs differ from generic ones. 1 https://github.com/nsg-ethz/axiom

4

Running time

Axiom : a logic programming language to express and enforce network designs

iBGP full mesh iBGP route reflection

1s

100 ms

Configuration

# lines

Design

Time

Memory

Single area, iBGP full mesh

4.58 M

generic specific

4.67 s 2.64 s

6.35 GB 4.19 GB

Four areas, iBGP full mesh

4.57 M

generic specific

5.46 s 2.69 s

6.65 GB 4.13 GB

Four areas, route reflection

0.05 M

generic specific

2.27 s 0.29 s

2.53 GB 0.27 GB

Number of routers 20

50

100

200

700

Figure 3: Axiom scales to large networks, checking their configurations within seconds. An iBGP full mesh needs almost 100 times more commands than route reflection, explaining the difference in checking time.

Table 1: Checking specific designs is easier than generic ones. We compare the running time and memory usage of Axiom to check specific or generic designs on the largest network in our dataset.

To answer them, we automatically generate Cisco configurations for all networks in TopologyZoo [27], the largest containing 754 routers. The configurations cover interface IP addresses, OSPF with one or multiple areas and virtual links, and iBGP sessions with either a full mesh or route reflection. We then write a generic Axiom design that accepts all combinations, and specific ones that pin down which variant is used and how. We run the experiments on an AMD EPYC server using 16 threads.

Axiom can scale to large networks. Figure 3 shows the running time of the specific designs with four OSPF areas on all networks in TopologyZoo. With route reflection, Axiom checks every network within 0.3 seconds, including the largest with 754 routers. The full mesh takes up to five seconds, but the cause is the input itself: a session between every pair of routers grows the largest configuration to 4.57 million lines, almost 100 times more than with route reflection. This is a stress test rather than a deployment; an iBGP full mesh across 754 routers does not scale [11]. As a comparison, Batfish [15] spends 12 minutes parsing the configurations and 3 simulating the network—more than two orders of magnitude longer than Axiom. This comparison illustrates the cost of computing network behavior, which Axiom’s approach avoids by checking the design directly.

The language of Axiom is concise and expressive. We split the design into three files, covering interfaces, OSPF, and iBGP, and write the latter two in a specific and a generic variant. The interface design relates devices: addresses must be unique, and connected interfaces must share a subnet. The specific OSPF design requires each area to be internally connected (a recursive property) and adjacent to the backbone. Further, it requires every interface address to be advertised. These two properties then establish reachability among all interface addresses. The specific iBGP designs rely on this reachability to guarantee all iBGP sessions can be established. We write two versions: one that requires a full mesh, resembling the example from section 2, and one where only the route reflectors need to form a full mesh, and all others have iBGP sessions with at least one reflector. The resulting .ax files need only 140 lines to check configurations of over 4 million lines. Of these, 19 templates and 18 rules model every command the designs use. The generic variant relaxes requirements for both OSPF and iBGP. OSPF no longer needs to advertise every interface; instead, the design propagates each network as far as the configuration allows. Whether two routers can establish an iBGP session now depends on whether they receive the other’s network. Instead of pinning down a specific topology, the iBGP design builds the propagation graph and asserts a valid path between all pairs of routers. Despite the added complexity, the design files have only 162 lines in total, and needs 8 additional rules compared to the specific design.

Specific designs yield cheaper checks and localized errors. Table 1 compares generic and specific designs on the largest network. The specific designs are cheaper to check: almost 2× for the iBGP full mesh, and 10× for route reflection, with a tenth of the memory. Derived facts drive memory usage: the generic designs require facts for OSPF routes and propagation paths, and the full mesh millions of session facts. With the specific design, Axiom accurately locates the errors; with the generic one, it reports only the high-level symptom, not the responsible command. When OSPF does not advertise an address needed by iBGP, the specific design reports the exact interface that is missing from OSPF, while the generic one reports that the IP address cannot be reached. When a full mesh misses a session, the specific design tells exactly which one, while the generic one warns that routes from either endpoint do not reach the other. Note that a verifier would report both errors as the same misbehavior: externally advertised routes would not be reachable.

6

RELATED WORK

Axiom relates to three lines of work: tools that, like Axiom, check the configuration itself; tools that check the behavior 5

Tibor Schneider and Laurent Vanbever

it produces; and programming languages to capture network computation or behavior.

it. We plan to instead let operators map such configuration objects to custom functions that the checker can call. Second, Axiom cannot yet interpret regular expressions embedded in configurations, like AS-path filters. Vendors define their own dialects, so the language must let operators define a dialect and then apply it. Evaluating a regex on concrete strings is then simple, as Datalog derives facts only forward. Some designs, however, need more: whether a filter drops every route with AS 666 in its path is a question about the regex itself, answered by inspecting its state machine rather than by testing strings.

Query-based configuration checking. Rcc [14] normalizes configurations into a database and queries it for predefined, known BGP faults. SelfStarter [24] flags outliers among similar configuration segments; it checks consistency, not intent. Further, it cannot relate one device’s configuration to another’s, say, a BGP neighbor command to the router owning that address. NCGuard [56] and Concord [8] instead let operators write their own conditions: NCGuard as queries over an XML representation of the configuration, and Concord as contracts attached to commands. Yet, both fail to capture network designs that involve properties on a graph as they lack recursive queries. Axiom checks everything these tools can, plus the recursive properties they cannot.

Negative provenance and synthesis. Y! [59] extends NDlog with negative provenance: it explains a missing route by the chain of facts that would have derived it. The technique transfers directly to Axiom, where a violated assert asks exactly that question: which facts are missing to correctly implement the design. We expect the answers to improve as well. In NDlog, almost any missing route can be forced with a static route, so explanations range over every configuration that could produce it, intended or not. A design admits only the intended mechanism, narrowing the explanation to, e.g., the missing iBGP session from Section 5. Negative provenance is the first step toward synthesis. Turning the missing facts into suggested commands requires reversing our templates: a def that matches commands must instead generate them. Applied repeatedly, such suggestions could complete a configuration from the design alone.

Behavioral verification and synthesis. Simulation [10, 15, 42, 49] computes the behavior of a configuration, and dataplane [19, 25, 26] and control-plane verification [5, 13, 18, 46, 48, 53, 58] check that behavior against the operators’ intent. Synthesis [1, 7, 12, 47] inverts the direction and generates configurations from the intended behavior. LLM-based management [21, 36, 57, 60] edits configurations directly and regains guarantees only by invoking a verifier in a loop. All these tools reason about what the network should do, but not how the configuration should achieve it. Yet, each keeps its place beside Axiom: simulation and verification can validate the design itself, and synthesis and LLMs can write configurations that Axiom holds to the design.

Ethical Concerns. This work raises no ethical concerns.

REFERENCES

Programming languages for networks. Propane [6] compiles routing policy into BGP configurations, leaving the design to its compiler. NetKAT [2, 17, 34] programs and verifies the data plane, never touching the configuration. NDlog [31] may appear closest to Axiom, as both extend Datalog; yet, it models the route computation itself and derives the routing state as its fixpoint. Even the semantics differ: NDlog expires sub-optimal paths by attaching timers to facts, while Axiom keeps fixpoints well-defined with lattices and stratification, which even our generic designs never exhaust. All three capture the network’s behavior or its computation; Axiom is their counterpart for its design.

7

[1] Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Aed: Incrementally synthesizing policy-compliant and manageable configurations. In Proceedings of the 16th International Conference on emerging Networking EXperiments and Technologies. 482–495. [2] Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic foundations for networks. Acm sigplan notices 49, 1 (2014), 113–126. [3] Michael Arntzenius and Neelakantan R Krishnaswami. 2016. Datafun: a functional Datalog. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 214–227. [4] Francois Bancilhon. 1986. Naive evaluation of recursively defined relations. In On knowledge base management systems: integrating artificial intelligence and database technologies. Springer, 165–178. [5] 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. 155–168. [6] Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2016. Don’t mind the gap: Bridging network-wide objectives and device-level configurations. In Proceedings of the 2016 ACM SIGCOMM Conference. 328–341. [7] Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2017. Network configuration synthesis with abstract

DISCUSSION AND OUTLOOK

We close by discussing what the language still misses and what it can borrow from declarative networking. Missing language features. Writing designs revealed two gaps in the language. First, configurations contain ordered lists of filters and transformations, like route-maps, where the first matching clause wins. Expressing them today takes a lattice to recover the order and recursive rules to walk 6

Axiom : a logic programming language to express and enforce network designs

topologies. In Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation. 437–451. [8] Ryan Beckett, Francis Y Yan, Raghunadha Reddy Pocha, Vineesh V Raj, Ayyub Shaik, and Siva Kesava Reddy Kakarla. 2026. Concord: Learning network configuration contracts. In Proceedings of the 21st European Conference on Computer Systems. 801–818. [9] Rüdiger Birkner, Dana Drachsler-Cohen, Laurent Vanbever, and Martin Vechev. 2020. Config2Spec: Mining Network Specifications from Network Configurations. In Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation. https: //www.usenix.org/conference/nsdi20/presentation/birkner [10] 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. 122–135. [11] Enke Chen, Tony J. Bates, and Ravi Chandra. 2006. BGP Route Reflection: An Alternative to Full Mesh Internal BGP (IBGP). RFC 4456. https://doi.org/10.17487/RFC4456 [12] Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2018. NetComplete: Practical Network-Wide configuration synthesis with autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). 579–594. [13] Seyed K Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. 2016. Efficient network reachability analysis using a succinct control plane representation. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). 217–232. [14] Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP configuration faults with static analysis. In Proceedings of the 2nd conference on Symposium on Networked Systems Design & Implementation-Volume 2. 43–56. [15] 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 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). 469–483. [16] Bryan Ford. 2004. Parsing expression grammars: a recognition-based syntactic foundation. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 111–122. [17] Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic netkat. In European Symposium on Programming. Springer, 282–309. [18] Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast control plane analysis using an abstract representation. In Proceedings of the 2016 ACM SIGCOMM Conference. 300–313. [19] Dong Guo, Shenshen Chen, Kai Gao, Qiao Xiang, Ying Zhang, and Y Richard Yang. 2022. Flash: fast, consistent data plane verification for large-scale network settings. In Proceedings of the ACM SIGCOMM 2022 Conference. 314–335. [20] Ashish Gupta, Inderpal Singh Mumick, and Venkatramanan Siva Subrahmanian. 1993. Maintaining views incrementally. ACM SIGMOD Record 22, 2 (1993), 157–166. [21] Rongxin Han, Jingyu Wang, Haifeng Sun, Zengteng Jiang, Qi Qi, Zirui Zhuang, Yuan Zhang, and Jianxin Liao. 2025. Network CoPilot: Intentdriven network configuration updating for service guarantee. In IEEE INFOCOM 2025-IEEE Conference on Computer Communications. IEEE, 1–10. [22] Pan Hu, Boris Motik, and Ian Horrocks. 2018. Optimised maintenance of datalog materialisations. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 32. [23] Santosh Janardhan. 2021. More details about the October 4 outage. https://engineering.fb.com/2021/10/05/networking-traffic/

outage-details/ Accessed: 13 July 2026. [24] Siva Kesava Reddy Kakarla, Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, Yuval Tamir, and George Varghese. 2020. Finding network misconfigurations by automatic template inference. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). 999–1013. [25] 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). 113–126. [26] Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2012. Veriflow: Verifying network-wide invariants in real time. In Proceedings of the first workshop on Hot topics in software defined networks. 49–54. [27] Simon Knight, Hung X Nguyen, Nickolas Falkner, Rhys Bowden, and Matthew Roughan. 2011. The internet topology zoo. IEEE Journal on Selected Areas in Communications 29, 9 (2011), 1765–1775. [28] 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. 210–217. [29] Zechun Li, Peng Zhang, Yichi Zhang, and Hongkun Yang. 2025. NDD: A Decision Diagram for Network Verification. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25). 237–258. [30] Hongqiang Harry Liu, Xin Wu, Wei Zhou, Weiguo Chen, Tao Wang, Hui Xu, Lei Zhou, Qing Ma, and Ming Zhang. 2018. Automatic life cycle management of network configurations. In Proceedings of the Afternoon Workshop on Self-Driving Networks. 29–35. [31] Boon Thau Loo, Tyson Condie, Minos Garofalakis, David E. Gay, Joseph M. Hellerstein, Petros Maniatis, Raghu Ramakrishnan, Timothy Roscoe, and Ion Stoica. 2009. Declarative networking. Commun. ACM 52, 11 (Nov. 2009), 87–95. https://doi.org/10.1145/1592761.1592785 [32] Magnus Madsen and Ondřej Lhoták. 2020. Fixpoints for the masses: programming with first-class Datalog constraints. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–28. [33] Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták. 2016. From datalog to flix: A declarative language for fixed points on lattices. ACM SIGPLAN Notices 51, 6 (2016), 194–208. [34] Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva. 2024. Katch: A fast symbolic verifier for netkat. Proceedings of the ACM on Programming Languages 8, PLDI (2024), 1905–1928. [35] Jeffrey C Mogul, Drago Goricanec, Martin Pool, Anees Shaikh, Douglas Turk, Bikash Koley, and Xiaoxue Zhao. 2020. Experiences with modeling network topologies at multiple levels of abstraction. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). 403–418. [36] Rajdeep Mondal, Alan Tang, Ryan Beckett, Todd Millstein, and George Varghese. 2023. What do llms need to synthesize correct router configurations?. In Proceedings of the 22nd ACM Workshop on Hot Topics in Networks. 189–195. [37] Boris Motik, Yavor Nenov, Robert Piro, and Ian Horrocks. 2015. Incremental update of datalog materialisation: the backward/forward algorithm. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 29. [38] Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev. 2025. Type-Constrained Code Generation with Language Models. In PLDI ’25: 46th ACM SIGPLAN International Conference on Programming Language Design and Implementation, Seoul, South Korea June 16-20, 2025. https://doi.org/10.1145/3729274

7

Tibor Schneider and Laurent Vanbever

[39] Ash Pallarito and Joe Abley. 2025. Cloudflare 1.1.1.1 incident on July 14, 2025. https://blog.cloudflare.com/cloudflare-1-1-1-1-incident-onjuly-14-2025/ Accessed: 13 July 2026. [40] The Batfish Open Source Project. 2026. Batfish Questions. https: //batfish.readthedocs.io/en/latest/questions.html Accessed: 17 July, 2026. [41] Ioannis Protogeros, Tibor Schneider, and Laurent Vanbever. 2026. Selfevolving network verifiers. In Proceedings of the 25th ACM Workshop on Hot Topics in Networks. [42] Bruno Quoitin and Steve Uhlig. 2005. Modeling the routing of an autonomous system with C-BGP. IEEE network 19, 6 (2005), 12–19. [43] Kenneth A Ross and Yehoshua Sagiv. 1992. Monotonic aggregation in deductive databases. In Proceedings of the eleventh ACM SIGACTSIGMOD-SIGART symposium on Principles of database systems. 114– 126. [44] Leonid Ryzhyk and Mihai Budiu. 2019. Differential Datalog. In Datalog 2.0. https://mihaibudiu.github.io/work/ddlog.pdf [45] Kemal Sanjta. 2023. Microsoft Outage Analysis: January 25, 2023. https://www.thousandeyes.com/blog/microsoft-outageanalysis-january-25-2023 Accessed: 13 July 2026. [46] Tibor Schneider, Jean Mégret, and Laurent Vanbever. 2025. Guided Exploration of Control-Plane Routing States. In 2025 IEEE 33rd International Conference on Network Protocols (ICNP). IEEE, 1–12. [47] Tibor Schneider, Roland Schmid, and Laurent Vanbever. 2022. On the complexity of network-wide configuration synthesis. In 2022 IEEE 30th International Conference on Network Protocols (ICNP). IEEE, 1–11. [48] 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). 1269–1287. [49] Tibor Jan Schneider. 2025. Extending the Limits of Formal Methods in Network Operations. Ph. D. Dissertation. ETH Zurich. [50] Yu-Wei Eric Sung, Xiaozheng Tie, Starsky HY Wong, and Hongyi Zeng. 2016. Robotron: Top-down network management at facebook scale. In Proceedings of the 2016 ACM SIGCOMM Conference. 426–439. [51] Tamás Szabó, Gábor Bergmann, Sebastian Erdweg, and Markus Voelter. 2018. Incrementalizing lattice-based program analyses in Datalog. Proceedings of the ACM on Programming Languages 2, OOPSLA (2018), 1–29. [52] Tamás Szabó, Sebastian Erdweg, and Gábor Bergmann. 2021. Incremental whole-program analysis in Datalog with lattices. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1–15. [53] Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman, Tejas Patil, Todd Millstein, and George Varghese. 2023. Lightyear: Using modularity to scale bgp control plane verification. In Proceedings of the ACM SIGCOMM 2023 Conference. 94–107. [54] 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. 748–761. [55] Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2024. Kirigami, the verifiable art of network cutting. IEEE/ACM Transactions on Networking 32, 3 (2024), 2447–2462. [56] Laurent Vanbever, Grégory Pardoen, and Olivier Bonaventure. 2008. Towards validated network configurations with NCGuard. In 2008 IEEE Internet Network Management Workshop (INM). IEEE, 1–6. [57] Changjie Wang, Mariano Scazzariello, Alireza Farshin, Simone Ferlin, Dejan Kostić, and Marco Chiesa. 2024. Netconfeval: Can llms facilitate network configuration? Proceedings of the ACM on Networking 2, CoNEXT2 (2024), 1–25.

[58] Dan Wang, Peng Zhang, and Aaron Gember-Jacobson. 2024. Expresso: Comprehensively reasoning about external routes using symbolic simulation. In Proceedings of the ACM SIGCOMM 2024 Conference. 197–212. [59] Yang Wu, Mingchen Zhao, Andreas Haeberlen, Wenchao Zhou, and Boon Thau Loo. 2014. Diagnosing missing events in distributed systems with negative provenance. ACM SIGCOMM Computer Communication Review 44, 4 (2014), 383–394. [60] Hao Zhou, Chengming Hu, Ye Yuan, Yufei Cui, Yili Jin, Can Chen, Haolun Wu, Dun Yuan, Li Jiang, Di Wu, et al. 2024. Large language model (llm) for telecommunications: A comprehensive survey on principles, key techniques, and opportunities. IEEE Communications Surveys & Tutorials 27, 3 (2024), 1955–2005.

8

Related documents

• Axiom: a logic programming language to express and enforce network designs#1468352
• ANALOGICAL AND DEPENDENCY DIRECTED REASONING STRATEGIES FOR LARGE SYSTEMS EVOLUTION#933641
• FailureAtlas: A Taxonomy of Failure Modes in Multi-Provider LLM Serving Infrastructure#386958
• Mitigating Error Propagation in Chain-of-Thought: A Tree-of-Thought Framework for Smart Contract Repair#482079
• The logic of perfection#1208667