Why "Ping Tests" Are Not Enough
Testing whether something can happen is easy — you send a packet and see if it arrives. Proving that something cannot happen is fundamentally harder. A ping test that succeeds proves reachability exists. A ping test that fails only proves that this specific packet was blocked — it says nothing about whether a different source IP, a different port, or a different protocol might still get through.
Formal verification solves this by analyzing the entire header space — every possible combination of source IP, destination IP, protocol, port, TCP flags, and other packet attributes. Instead of testing one packet at a time, Batfish reasons about all possible packets simultaneously.
A concrete example:
Suppose your security policy says: "Block all SSH (TCP port 22) from the internet to internal servers."
You write this ACL:
ip access-list extended INTERNET_IN
10 deny tcp any 10.0.0.0 0.255.255.255 eq 22
20 permit ip any any
A ping test won't catch the problem here. But Batfish will: line 20 permits all IP traffic, which includes TCP port 22. The deny on line 10 only blocks SSH to the 10.0.0.0/8 range. If your servers are on 192.168.1.0/24, they're completely unprotected. Batfish enumerates all possible packet headers and finds the gap.
The "buried permit" problem: ACLs are evaluated top-to-bottom, first-match. A common bug is a broad permit ip any any rule buried hundreds of lines into a long ACL that accidentally overrides specific deny rules above it — but only for traffic that doesn't match any of the earlier rules. This is nearly impossible to catch by reading the ACL manually. Batfish catches it instantly.
A common SRE/network interview question is: "How do you verify that a security policy is actually enforced in your network?" The answer that impresses is: "I use formal verification tools like Batfish to perform exhaustive header-space analysis. Unlike ping tests, which only verify specific flows, Batfish proves that no packet matching a prohibited pattern can traverse the network — it's a mathematical guarantee, not a sample."