Runbooks are not proofs: checking actions against live state
Most unsafe maintenance actions look safe in isolation. Here is why the check has to see in-flight work and lost backup paths.
Before an engineer drains a switch, the runbook asks a sensible question: is this device redundant? If the answer is yes, the drain proceeds.
In our study of 2,000 random maintenance scenarios on a Clos network, that check approved 98.4% of the actions that were actually unsafe. The runbook was not wrong about the device. It was wrong about the network.
Three things the runbook cannot see
- Concurrent work. A drain that is safe on its own becomes dangerous if someone is draining the device's partner in another change.
- Existing failures. If a neighboring device is already down, the redundancy the runbook is counting on has already been spent.
- Lost backup paths. Even when every server stays reachable, an action can leave some of them single-homed — violating a requirement that matters as much as reachability.
These are not exotic situations. They are the normal state of a large network on a busy maintenance night.
Defining "safe"
To check an action you need a precise definition of harm. We used a simple rule: for every server, resilience after the action must be at least the smaller of its resilience before and its required level.
resilience_after ≥ min(resilience_before, required_level)Resilience here means the number of device-disjoint paths from the server to the network core, capped at two. Two means the server survives any single further device failure. One means it does not.
The rule is deliberately forgiving about the past: if a server is already down to one path because of an earlier failure, the action is not blamed for that. It is only responsible for the harm it adds.
Five ways to check
| Method | Sees live state | Sees backup paths | Exact |
|---|---|---|---|
| Runbook | No | No | No |
| State-aware reachability | Yes | No | No |
| Brute force | Yes | Yes | Yes — O(V·(V+E)) |
| Max-flow per server | Yes | Yes | Yes |
| Block-cut tree | Yes | Yes | Yes — O(V+E) |
The two approximate checks fail in different ways. Of the 744 unsafe actions in our test set, 168 would have disconnected servers outright; the runbook approved 156 of those, while the state-aware check caught all of them. The other 576 unsafe actions only removed backup paths — and both approximate checks approved every one. Exact methods approved none.
The trick: one graph pass
Exact checks are usually dismissed as too slow for live operations, and max-flow per server bears that out: 218 seconds for a 3,672-device network. But there is a classical shortcut.
Add a virtual node connected to every core router. By Menger's theorem, a server has two device-disjoint paths to the core exactly when it and that virtual node sit in the same biconnected component of the graph. Biconnected components can be found for the whole graph in a single depth-first search — Hopcroft and Tarjan, 1973.
| Network | Devices | Max-flow | Block-cut tree |
|---|---|---|---|
| 4 pods | 60 | 0.03 s | 0.0005 s |
| 64 pods | 920 | 9.2 s | 0.008 s |
| 256 pods | 3,672 | 218 s | 0.04 s |
| 1,024 pods | 14,680 | — | 0.19 s |
Nothing here is new mathematics. Menger's theorem is from 1927. What is new is applying it at the moment of action, against live state, to every proposed change.
Adaptive formal verification
We call this adaptive formal verification: rather than checking an action against a static policy written in advance, re-check it against the network as it actually is, including every failure and in-flight change, right before it runs.
Three properties make it practical. It gives a mathematical guarantee for the property it checks. It does not care who proposed the action — a human, a script or a model — which matters as more remediation is suggested by automated systems. And it explains itself: "server p3-srv-1-2 would drop from 2 paths to 1; required 2."
What it does not cover
This check is about connectivity and redundancy. It does not reason about routing policy, ACLs, VLANs or capacity; those need configuration modeling, typically with SMT solvers. It handles device failures, not individual link cuts. It was tested on regular Clos topologies; carrier rings and meshes need their own validation. Resilience requirements above two need max-flow.
Those are the next steps, starting with real customer topologies. The research note has the details, and Verified Remediation shows how the check is used in the platform.