NETLEMMA / KANIT2026 — 001
Prove a network change before it goes live.
[ K / 01 ]
Describe the change in plain language. Claude writes the configuration change and Batfish verifies it against a model of your network. You only see changes that passed.
Early prototype. Works today for Cisco IOS access lists.
01 / Chapter
Live proof record
Open tcp/5432 from the user network to the database server (10.20.20.30).
Open tcp/5432 from the user network to the database server (10.20.20.30).
ip access-list extended SERVERS-OUT
permit tcp 10.10.10.0 0.0.0.255 host 10.20.20.10 eq 443
permit tcp 10.10.10.0 0.0.0.255 host 10.20.20.20 eq 22
+permit ip 10.10.10.0 0.0.0.255 host 10.20.20.30 deny ip any any- Users reach the database on tcp/5432proved
- The internet cannot reach the server networkproved
- Users cannot SSH to the database serverviolatedCounterexample: 10.10.10.0:49152 → 10.20.20.30:22 TCP (SYN) => DELIVERED_TO_SUBNET
02 / Chapter
How it works
Process / 03 steps
- 01
Claude writes the change
It reads your current configurations and rules, then produces the narrowest change that meets the request, plus the flow checks that would prove it.
- 02
Batfish verifies it
The change is applied to a model of the network. Each check is tested over the whole set of flows, not sample packets; anything that breaks comes back as a concrete counterexample.
- 03
The counterexample goes back
A rejected proposal is returned to Claude with the reason and gets fixed. If nothing passes, your configuration is left untouched.
03 / Chapter
Short demo
Run it locally
The demo recording is not ready yet.
Until it is, you can run the same flow on your own machine: the overly broad proposal is rejected with a counterexample and the narrow one is accepted. Docker and Python are enough; no API key needed.
Command
make setup && make demo04 / Chapter
Boundary of proof
Limits
What it proves
- 01That every flow the request requires is reachable, or blocked.
- 02That the invariant rules you defined still hold after the change.
- 03That the change adds no parse errors or undefined references.
- 04It also lists example flows whose behaviour changed, before and after.
What it does not
- 01It cannot know a rule you never wrote down. Protection is only as strong as your invariants.
- 02Devices and features Batfish does not model are out of scope.
- 03The model is built from configuration; it does not see runtime problems such as hardware faults or software bugs.
- 04A person gives the final approval. The tool never pushes to a device itself.
Pilot access is open
Try it on your own network
Your configurations stay with you: verification runs on a Batfish instance on your own machine. We are looking for our first pilot teams.
Write to us about a pilot