Scenario proofs simplify checking distributed protocol correctness
Scenario Proofs for Verification of Distributed Protocols
Programming Languages
Summary
Verifying that distributed computer systems work correctly is hard because they can behave in many ways. The authors introduce a method called scenario proofs that focuses on typical example runs rather than all possible states. They create structured descriptions of these example runs and prove that all real runs match one of them. Then they check correctness only on these representative examples, making verification clearer and easier to understand. This connects well to how designers usually think about these systems.
What this means in practice
- •For distributed systems engineers: Verify complex distributed protocols with clearer reasoning over representative scenarios instead of complicated exhaustive state invariants.
- •For cloud infrastructure teams: Improve correctness proofs of distributed coordination services using scenario proofs that align with design-phase causal reasoning.
Authors
Zhendong Ang, George Pîrlea, Umang Mathur
Abstract
Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreachable states. This burden is often misaligned with how protocol designers reason: they explain correctness by following representative executions, causal histories, and phase-structured interactions among nodes. This paper introduces scenario proofs, a verification methodology that makes such execution-oriented reasoning formal. A scenario is a structured expression describing representative protocol executions, enriched with ghost variables. Rather than enumerate all possible interleavings, a scenario describes canonical executions and uses a sound semi-commutation relation to account for reorderings that preserve feasibility and final states. Verification then factors into two main obligations. Coverage shows that every feasible protocol execution is equivalent, up to semi-commutation, to one described by the scenario; this obligation is independent of the safety property and serves as a reusable behavioral characterization of the protocol. Correctness proves the desired safety property only over the representative executions, using Hoare-style weakest-precondition reasoning along the scenario structure. We formalize the scenario language, its layered semantics, and proof rules for coverage and correctness. Through case studies of ring leader election, two-phase commit, a decentralized lock, two variants of multi-signature payment, and single-decree Paxos, we show how scenario proofs capture the causal and phase-based arguments used informally by protocol designers. These examples illustrate that scenario proofs can replace monolithic invariant discovery with structured reasoning over representative executions, while retaining a rigorous connection to all feasible protocol behaviors.