Proving safety properties of distributed protocols traditionally requires finding inductive invariants that are preserved by every protocol action in isolation, a style of reasoning that is disconnected from how protocol designers argue about correctness. We propose \emph{scenario-based proof}, a methodology that formalizes execution-oriented reasoning. The user writes a \emph{scenario}, a structured expression in a KAT-like language describing representative executions of the protocol. The proof reduces to two obligations: \emph{coverage}, that the scenario’s commutativity closure contains all protocol executions, and \emph{correctness}, that every execution described by the scenario maintains the safety property. We exploit semi-commutativity of independent actions so that the scenario only describes canonical execution orders. We develop a formal proof system that extends Kleene Algebra with Tests with commutativity rewriting rules and semantic reasoning, and mechanize the methodology in Lean 4.