Testing Without a Network
How do you test a network change without a physical network? You build a mathematical model of the network and reason about it symbolically. This is called Formal Verification — the same technique used to verify CPU designs and safety-critical software.
Batfish is the leading open-source tool for network formal verification, originally developed at Microsoft Research and now maintained by Intentionet. It ingests your configuration files and builds a complete in-memory model of how the network would behave if those configs were applied.
How Batfish works, step by step:
-
Input: You provide Batfish a directory of configuration files — Cisco IOS, Juniper JunOS, Arista EOS, AWS VPC configs, Palo Alto firewall rules, etc. These are the same text files that would be deployed to real devices.
-
Parsing: Batfish parses each file and extracts the structured data: interface addresses, routing protocol configurations (BGP, OSPF, IS-IS), ACL rules, NAT policies, and more.
-
Control Plane Modeling: Batfish simulates routing protocol convergence. It calculates what the routing tables would look like after BGP and OSPF finish exchanging routes — without actually running BGP or OSPF.
-
Data Plane Modeling: Using the converged routing tables and ACL rules, Batfish builds a model of the data plane — for every possible packet, which path would it take, and would it be permitted or denied?
-
Query Interface: You ask Batfish questions using Python (
pybatfishlibrary) or a REST API. It answers by solving logic problems against its model.
Config Files (text)
↓
Batfish Parser
↓
Network Model (in-memory)
├── Control Plane (routing tables)
└── Data Plane (ACLs, forwarding)
↓
Python Queries (pybatfish)
↓
Answers: reachability, loops, policy violations
Batfish never sends a single packet. It doesn't need a network. It solves the problem the way a mathematician solves an equation — by reasoning about the structure of the problem itself.