Formal Verification of Circuit-Breaker Fleets Under Two Downstream Overload Semantics

Abstract

Circuit breakers protect a downstream dependency from a fleet of independent clients that retry after a shared failure. Engineering practice recommends adding jitter to the breaker's open-timeout so the fleet does not retry in lockstep, but the strength of this recommendation is rarely stated precisely: is jitter merely an efficiency improvement, or is it required for correctness? We show the answer depends on an assumption about the downstream dependency that is easy to leave implicit. Under fail-together overload semantics, where a batch of concurrent probes exceeding the dependency's capacity fails in its entirety, an unjittered fleet never recovers: explicit-state model checking finds a permanent livelock in every one of 14 tested fleet configurations. Under admission-control semantics, where only the first C arrivals of an overloaded batch are served, the same fleet always recovers, and jitter is merely beneficial: the exhaustive model predicts a 1.7x to 3.8x recovery speedup depending on fleet size, and an independent asyncio prototype confirms the effect directly, measuring a 2.2x speedup for the two fleet sizes it tests. We give a deterministic, modulo-based jitter assignment, prove its round-one safety bound by a pigeonhole argument cross-checked independently in Z3, and report a residual transient-overload limitation left open for future work.