papers/lux-model-checking-tla/sections/01-why-model-checking.tex

\section{Why Model Checking}


\subsection{The Problem with Distributed Systems}

Distributed systems are hard because they have \emph{combinatorial} behavior. A system
with $n$ nodes and $m$ messages has $O(m!)$ possible message orderings. Each ordering
may produce different behavior. Testing exercises a handful of orderings; model checking
exercises all of them.

\subsection{What Model Checking Provides}

Given a system description $S$ and a property $P$, a model checker answers: does $P$
hold in every reachable state of $S$? If yes, it provides a proof (by exhaustive
enumeration). If no, it provides a \emph{counterexample trace}: a sequence of states
from the initial state to a state where $P$ is violated.

Counterexample traces are the primary value of model checking. A trace that shows
``node~A sends message~X, node~B crashes, node~C receives message~Y before message~X,
and now the system is in an inconsistent state'' is worth more than a thousand tests.

\subsection{Model Checking vs.\ Theorem Proving}

Model checking is \emph{automatic}: you write the spec, push a button, and get a yes/no
answer. Theorem proving (Lean~4, Coq) is \emph{manual}: you guide the prover through
the argument. Model checking is limited to finite instances (e.g., 4 validators, 3 rounds);
theorem proving handles arbitrary sizes. Use both: model check to find bugs during design,
then prove correctness for the final protocol.

%% ============================================================