LoopGuard protects against a specific failure: a redundant port stops receiving BPDUs while its physical link remains live. Without protection, the port can self-promote into a forwarding state and close a physical loop. LoopGuard refuses that promotion and keeps the port Blocking.
The question looked temporal
A network can evolve through link failures, BPDU loss, recovery, and repeated flapping. That naturally suggests a coalgebraic model: states transition through events, and a safe implementation should behave correctly along every possible trajectory. One might formulate the goal as a bisimulation between the guarded system and an ideal always-safe reference.
Formalizing the reference computation surfaces an important simplification. The role-assignment function is memoryless. It recomputes roles from the current physical topology, perceived topology, configuration, and failure snapshot. It does not remember which sequence of events produced that snapshot.
Two topologies, two kinds of failure
The model starts from a denotational STP computation that assigns Root, Designated, and Blocking roles. A dynamic state is a pair: the ports currently losing BPDUs and the links that are physically down.
These failure types are deliberately kept separate. A down link is removed from the physical topology. A BPDU-lost port still has a live physical link, but that link is removed from the perceived topology used by the role computation. Loop safety is checked against the physical topology, because that is where a real cycle would exist.
The snapshot safety theorem
Assume the perceived topology remains connected. If every physically present link missing from the perceived topology has LoopGuard configured on at least one endpoint, then the active-role subgraph contains no cycle.
The proof is direct. The perceived topology receives an ordinary STP spanning tree, call it T. Every link missing from that perceived topology is processed by the failure rule. The hypothesis guarantees that at least one endpoint of every such link is guarded, so the link remains inactive. The physical active subgraph is therefore exactly T, which is connected and acyclic.
Exhaustive mechanization
The theorem was implemented in Haskell by extending the existing static role-assignment code. The checker enumerated every combination of BPDU-lost ports and physically down links for two small topologies: a guarded triangle and a guarded four-switch ring.
The hypothesis held for 125 of 512 triangle snapshots and 625 of 4,096 ring snapshots. Every one of those 750 snapshots was loop-free. This is an exhaustive check for these topologies, not a sample intended to stand in for proof or generality.
rolesUnderFailure :: Graph -> Config -> State -> Roles
rolesUnderFailure graph config state =
assignPortRoles (perceived graph state) config
safeSnapshot graph config state =
connected (perceived graph state)
&& guardedMissingLinks graph config stateA useful correction
Exhaustive checking also caught an initially plausible but false necessity claim. Violating the LoopGuard hypothesis does not always produce a loop. On the unguarded triangle, 387 of 512 snapshots violated the hypothesis, but only 63 produced a loop. On the unguarded four-switch ring, 3,471 violations produced only 255 loops.
Multiple simultaneous failures can leave an active tree that does not allow a missing link to close a cycle. The theorem is therefore a sufficient condition, not a characterization of every unsafe state. Reporting that correction is part of the result: exhaustive checking prevented the stronger false claim from becoming part of the final argument.
What remains genuinely temporal
A real temporal LoopGuard model would need state that persists across events: timers, hysteresis, recovery delays, and behavior under links that flap faster than the protective timer. In that setting, a port’s behavior would depend on how long it has been silent and on its transition history. Bisimulation would become relevant again because the current snapshot would no longer determine the complete observable behavior.
Limitations and next steps
Necessity is not fully characterized, BPDU loss is modeled as symmetric silence, and only two small synthetic topologies were checked. The perceived-topology-connected assumption also excludes network partitions, which are a separate failure mode.
The next step is a timed model with real memory. That would test whether the snapshot safety guarantee survives timers and fast link flapping, and would answer the coalgebraic question that the memoryless model makes unnecessary.