# Model Checking in Practice

> Write a real spec, understand exhaustive state-space exploration, and see a genuine concurrency bug a model checker catches before code exists.


---

# Model Checking in Practice

[Formal Methods and Specification](/guides/formal-methods-and-specification) introduced the
mental model: states, transitions, invariants, liveness, and a first look at exhaustive checking.
This guide is the follow-up for someone who read that and wants to actually do it - write a
complete spec for something real, understand what a checker is doing mechanically when it
"explores every state," and watch it catch a genuine concurrency bug.

Read the prerequisite first if you haven't. This picks up exactly where it left off and doesn't
re-explain states, transitions, or the safety/liveness split.

## How to read this

- **Want the full worked spec?** [Phase 1](01-writing-a-real-spec.md) specifies a mutual-exclusion
  lock end to end - state, transitions, a safety property, and a liveness property.
- **Want the mechanics of checking?** [Phase 2](02-exhaustive-state-space-exploration.md) covers
  how a checker actually walks a state graph, and the state explosion problem - in plain terms.
- **Want to see it catch something real?** [Phase 3](03-a-real-concurrency-bug-caught-before-code.md)
  walks a genuine lost-update race a model checker finds that a human reviewer would not, and where
  model checking still can't save you.

## The phases

1. **[Writing a Real Spec](01-writing-a-real-spec.md)** - a mutual-exclusion lock, specified
   completely: states, transitions, a named safety property, and a named liveness property.
2. **[Exhaustive State-Space Exploration](02-exhaustive-state-space-exploration.md)** - what a
   checker does step by step, why that's fundamentally not testing, and why state explosion is a
   real ceiling you can work around.
3. **[A Real Concurrency Bug, Caught Before Code](03-a-real-concurrency-bug-caught-before-code.md)**
   - a classic lost-update interleaving, the counterexample that finds it, and the real limits of
   the whole approach.

> Prerequisite: [Formal Methods and Specification](/guides/formal-methods-and-specification) -
> especially its states/transitions/invariants phase
> ([Phase 2](/guides/formal-methods-and-specification/2)) and its checking phase
> ([Phase 3](/guides/formal-methods-and-specification/3)). Also builds on
> [What Logic Actually Is](/guides/what-logic-actually-is) and
> [Predicate Logic and Quantifiers](/guides/predicate-logic-and-quantifiers).


---

# Writing a Real Spec

The prerequisite guide specified a turnstile and sketched a money-transfer system. Both stopped
short of a full spec you could hand to a checker - the transfer system listed invariants without
nailing down every transition. This phase closes that gap: one system, specified completely enough
that nothing is left to "we'll figure it out later."

The system: two processes, `P1` and `P2`, sharing one resource - a database connection, a critical
section, whatever. Only one may hold it at a time. This is mutual exclusion, the most-studied
problem in concurrent systems, because almost every lock, mutex, and semaphore you've ever used is
an implementation of it.

## The state

Each process has a **location** - which line of its own logic it's currently at - and there's one
shared variable for who holds the lock.

```text
VARIABLES
  loc[P1], loc[P2]     \* each process's current location
  lock                 \* holder of the lock, or "none"

Locations for each process:
  idle       -- not trying to enter
  waiting    -- wants the lock, hasn't gotten it yet
  critical   -- holds the lock, running its critical section
```

A full state is a snapshot of all three: `(loc[P1], loc[P2], lock)`. With 3 locations per process
and 3 possible lock values (`none`, `P1`, `P2`), the raw grid is 27 combinations - most of them
unreachable, which phase 2 comes back to.

Two processes is the smallest interesting case, and that's deliberate. A spec for "N processes"
reads almost the same on paper but explores a state space that grows with N - phase 2 is where
that growth becomes the whole story. Fix N at 2 for now and get the transition rule exactly right;
generalizing the count is mechanical once the rule is correct.

## The transitions

Each process moves through the same three-step cycle, and the transition rule is what actually
enforces exclusion (or fails to).

```text
For process P (with the other process Q):

  T1_request:  loc[P] = idle  ->  loc[P] = waiting
               (P decides it wants the lock; always enabled)

  T2_acquire:  loc[P] = waiting  AND  lock = none
               ->  loc[P] = critical,  lock = P
               (P may only take the lock if nobody holds it)

  T3_release:  loc[P] = critical
               ->  loc[P] = idle,  lock = none
               (P finishes and gives the lock back)

Init:  loc[P1] = idle,  loc[P2] = idle,  lock = none
```

*What just happened:* `T2_acquire` is the entire mechanism. Its guard - `lock = none` - is a
precondition that must hold before the transition can fire. Take that guard away and you no longer
have a mutual-exclusion protocol, you have two processes racing to overwrite the same variable.
Writing the guard down explicitly is the spec-writing skill: everything about "correctness" here
lives in one line.

Note what's absent: no scheduler, no thread priority, no timing. At each step, *any* process with
an enabled transition may fire - the checker will try every process, every order, every
interleaving, not only the one you'd naturally imagine.

This is a real design choice, not laziness. Real schedulers are complex and vary by OS, language
runtime, and hardware. If the spec baked in a specific scheduling policy, a clean check would only
tell you the protocol is correct *under that policy* - and the moment you deploy on a different
runtime, or a future kernel version changes its scheduling heuristics, the guarantee evaporates.
Assuming an arbitrary, adversarial scheduler is stricter than any real one, so a protocol proven
correct against "anything can happen next" is correct against whatever scheduler you actually get.

## The safety property: mutual exclusion itself

Name the thing that must never happen, precisely:

```text
MutualExclusion ==
  NOT (loc[P1] = critical AND loc[P2] = critical)

  "It is never the case that both processes are in
   their critical section at the same time."
```

This is a one-line invariant, and it's the entire point of the system. Every mutex, database lock,
and distributed lock manager you've used exists to make this true. If a checker ever finds a
reachable state where both locations read `critical`, the lock is broken, full stop - no
disclaimers, no "well it's probably fine in practice."

## The liveness property: nobody waits forever

Safety alone permits a useless protocol: if `T2_acquire` never fires for `P2` at all, `P1` can hog
the lock forever and `MutualExclusion` never breaks. That's safe and worthless. Liveness rules it
out:

```text
LockFreedom ==
  (loc[P1] = waiting) ~> (loc[P1] = critical)
  (loc[P2] = waiting) ~> (loc[P2] = critical)

  "If a process is waiting, it eventually reaches
   its critical section."  (~> reads "leads to")
```

*What just happened:* `~>` is shorthand for "eventually" chained onto a condition - if the
left side ever becomes true, the right side must become true at some later point. This is the
"something good eventually happens" property from the prerequisite guide, made concrete for a lock:
waiting is not the same as starving.

A protocol can satisfy `MutualExclusion` and violate `LockFreedom` at the same time - that
combination is exactly what phase 3 goes looking for, because it's the failure mode nobody tests
for. Nobody writes a unit test titled "assert this thread doesn't wait forever," because a test
that hangs looks like a timeout, not a design flaw.

## Why this is a complete spec

Four ingredients, all present: variables (`loc`, `lock`), an initial state (`idle`/`idle`/`none`),
transitions with explicit guards (`T1`-`T3`), and two properties of different flavors
(`MutualExclusion`, `LockFreedom`). Nothing about *how* `lock` is implemented - no compare-and-swap,
no OS primitive - because the spec doesn't need to know. It only needs the rule that governs when
the lock may change hands. That's the level phase 2 will search exhaustively.

```quiz
[
  {
    "q": "What does the guard `lock = none` on transition T2_acquire actually do?",
    "choices": [
      "It's documentation only, with no effect on behavior",
      "It's the precondition that must hold before P can take the lock - the entire exclusion mechanism",
      "It slows down the process",
      "It only matters for the liveness property"
    ],
    "answer": 1,
    "explain": "The guard is a precondition: the transition is only enabled when it's true. Removing it removes mutual exclusion entirely - both processes could acquire the lock at once."
  },
  {
    "q": "A protocol never lets two processes hold the lock at once, but one process can wait forever while the other repeatedly re-acquires it. What's true?",
    "choices": [
      "The protocol violates MutualExclusion",
      "The protocol satisfies MutualExclusion but violates LockFreedom",
      "The protocol violates both properties",
      "This can't happen if the spec is written correctly"
    ],
    "answer": 1,
    "explain": "Never colliding is safety, intact here. But the waiting process never reaching critical is exactly what LockFreedom (a liveness property) forbids - safety and liveness fail independently."
  },
  {
    "q": "Why does the spec avoid describing how `lock` is implemented (compare-and-swap, OS mutex, etc.)?",
    "choices": [
      "Because implementation details are irrelevant to what's being reasoned about - only the rule governing when the lock changes hands matters",
      "Because TLA+ cannot express implementation details",
      "Because it would make the spec too short",
      "Because compare-and-swap is always correct anyway"
    ],
    "answer": 0,
    "explain": "The spec strips away 'how' on purpose - it keeps the rule that matters (the guard on T2_acquire) and discards the mechanism that enforces it in real code, per the blueprint/building split from the prerequisite guide."
  }
]
```


---

# Exhaustive State-Space Exploration

You have a complete spec from phase 1. Now: what does a checker actually *do* with it? Not the
one-sentence version from the prerequisite guide - the mechanism, concretely, including the part
where it stops scaling and why that's an acceptable trade rather than a fatal flaw.

## The algorithm is almost embarrassingly simple

A model checker runs a breadth-first search over the state graph. That's the whole trick:

```text
1. Put the initial state in a queue. Mark it "seen."
2. Take a state off the queue.
3. For each transition that's enabled in this state:
     a. Compute the resulting state.
     b. Check every invariant against it. If one fails, STOP and report
        the path from INIT to here (the counterexample).
     c. If this resulting state hasn't been "seen" before, mark it seen
        and add it to the queue.
4. If the queue is empty, every reachable state has been visited
   and every invariant held everywhere. Done.
```

Apply this to the lock spec from phase 1. `INIT` is `(idle, idle, none)`. Two transitions are
enabled - `T1_request` for `P1` or for `P2` - so the search branches into two states,
`(waiting, idle, none)` and `(idle, waiting, none)`. Each of those branches again. The graph fans
out exactly as far as the transitions allow, and the checker visits every node in it exactly once.

There's no cleverness about *which* interleaving matters. It doesn't reason about "the tricky
case" - it has no notion of tricky. It enumerates. That's the entire source of its power: your
intuition prunes the search space based on what seems plausible, and the plausible-looking branches
are rarely where the bug hides.

## This is not testing with more steps

Testing samples. You write a scenario - `P1` requests, `P2` requests, `P1` acquires, `P1` releases,
`P2` acquires - run it once, and it either matches expectations or it doesn't. Add ten more
scenarios and you've sampled eleven paths through a graph that might contain thousands.

A checker doesn't pick paths. It computes the entire reachable set. For the two-process lock, "the
entire reachable set" is small enough to write out - roughly a dozen states, once you exclude the
27-combination raw grid's unreachable entries (you can never have `lock = P1` while `loc[P1] = idle`,
for instance; nothing produces that combination). The checker doesn't know that shortcut in advance.
It discovers it by trying every transition from every state it finds and never generating the
unreachable ones in the first place.

The guarantee that falls out of this is categorically different from a test suite's guarantee. "All
eleven tests pass" means eleven paths are fine. "Model checking completed" means *every* path is
fine - there is no twelfth path you forgot to write, because the search doesn't work by you writing
paths.

## The state explosion problem

Here's the catch. The lock example has two processes and three locations each. Bump it to
five processes and the raw combinations jump from 27 (3 x 3 x 3 lock values) to roughly 3 x (3^5)
location combinations - already over 700, and that's before counting the unreachable ones out. Add
a counter that can hold values 0 to 99, and multiply again. State spaces grow **multiplicatively**
with every extra variable and **combinatorially** with every extra concurrent process, because the
checker has to consider every process at every possible location relative to every other process.

This is not a tooling limitation that better engineering fixes. It's inherent to what exhaustive
search means. A real distributed system - a consensus protocol with a dozen nodes, message queues,
retries, timeouts - has a state space that dwarfs the number of atoms worth counting. No amount of
RAM or clever indexing makes "visit literally every one" tractable at that scale.

Model checkers fight back with real techniques - symmetry reduction (treating identical processes as
interchangeable so you don't re-explore the same shape relabeled), partial-order reduction (skipping
interleavings that provably can't affect the outcome), and abstraction (replacing "a counter from 0
to 99" with "zero, one, many" when the exact number doesn't matter to the property). These push the
ceiling up. They don't remove it.

## Why this is fine

The instinct here is to conclude model checking "doesn't scale" and shelve it. That's the wrong
lesson. You don't model-check your whole application - you never did, and nobody who uses this well
tries to. You model-check the one dangerous piece: the lock, the consensus core, the payment state
machine, the two functions where a race would actually hurt. That component's state space, bounded
to a handful of participants, is exactly the size the algorithm above handles in seconds.

The lock spec from phase 1, checked with two processes, isn't a toy because it's small - it's small
*because that's the right scope*. The two-process case already contains every interleaving pattern
the protocol's logic can produce; a twentieth process doesn't add a new *kind* of bug, it adds more
copies of the same kinds you'd already catch at two or three. Engineers who use model checking
professionally bound their models on purpose - "up to 4 nodes," "up to 3 in-flight requests" - and
treat a clean result at that bound as strong evidence about the design, not a claim about every
deployment size on earth.

```quiz
[
  {
    "q": "What search algorithm does a model checker use to explore the state space?",
    "choices": [
      "It randomly samples states, like fuzzing",
      "Breadth-first search: visit the initial state, then every state reachable in one step, then two steps, and so on",
      "It asks the developer which states to check",
      "Depth-first search down a single chosen path"
    ],
    "answer": 1,
    "explain": "The checker does breadth-first search from the initial state, checking invariants at every newly discovered state, until the queue of unvisited states is empty."
  },
  {
    "q": "Why does adding more concurrent processes make the state space grow so fast?",
    "choices": [
      "It doesn't - state space size is independent of process count",
      "Because the checker has to consider every process at every possible location relative to every other process, which multiplies combinations",
      "Because more processes means more code to compile",
      "Because the checker re-runs the entire search once per process"
    ],
    "answer": 1,
    "explain": "Each added process multiplies the number of location combinations, so the state space grows combinatorially with concurrency - this is the state explosion problem."
  },
  {
    "q": "Why is state explosion not a reason to abandon model checking?",
    "choices": [
      "Because RAM is cheap enough to brute-force any state space eventually",
      "Because you bound the model to the one risky component (a lock, a protocol core) rather than the whole system, and that's usually small enough to check completely",
      "Because state explosion only affects languages other than TLA+",
      "Because testing has the same limitation, so it doesn't matter"
    ],
    "answer": 1,
    "explain": "Practitioners scope model checking to the dangerous, concurrency-heavy component and bound the model (e.g. up to N processes), which keeps the space checkable while still catching the interleaving bugs that matter."
  }
]
```


---

# A Real Concurrency Bug, Caught Before Code

Phase 2 explained the mechanism. This phase runs it on a genuine bug pattern - one that has shipped
in real connection pools, semaphore implementations, and reference-counted resource managers - and
then gets clear-eyed about where model checking stops helping.

## The system: a bounded resource pool

A pool holds `N` interchangeable resources (database connections, worker threads). Processes check
one out, use it, and check it back in. The pool tracks how many are currently in use with a shared
counter, and refuses a checkout once the counter hits the limit.

```text
VARIABLES
  inUse           \* shared counter: how many resources are checked out
  loc[P1], loc[P2]

LIMIT == 1        \* pool size 1, to isolate the bug with the fewest moving parts

Locations:
  idle, reading, writing, holding, done

T1_read_count:   loc[P] = idle
                 -> loc[P] = reading   (read current value of inUse into a local)

T2_check_and_inc: loc[P] = reading  AND  localCount < LIMIT
                 -> loc[P] = writing  (decided there's room; about to write it back +1)

T3_write_inc:    loc[P] = writing
                 -> inUse' = localCount + 1,  loc[P] = holding

T4_release:      loc[P] = holding
                 -> inUse' = inUse - 1,  loc[P] = done
```

*What just happened:* this is "read, check, then write" split into three separate steps -
`localCount` is a per-process local variable holding what `inUse` looked like at read time. That
split is the bug. Real code does this whenever a check and an update aren't a single atomic
instruction: read a counter, decide there's capacity, then write the incremented value back.

## The invariant nobody would think to violate

```text
PoolInvariant ==
  inUse <= LIMIT

  "The pool never reports more resources checked out than it has."
```

Trivially true if only one process ever runs `T1` through `T3` at a time. The whole reason to
write a spec is to stop assuming that and check every interleaving instead.

With `LIMIT == 1` and two processes, the raw state space here is small - a handful of location
pairs times a few values of `inUse` - well within what phase 2 called checkable in seconds. That's
the point: you don't need a large model to expose this bug, you need the *right* one. A bigger pool
size or a third process would multiply the state count without teaching the checker anything new
about this particular flaw.

## The interleaving

```text
Step 0  INIT        inUse=0   loc[P1]=idle      loc[P2]=idle
Step 1  P1: T1       inUse=0   loc[P1]=reading   (P1's localCount = 0)
Step 2  P2: T1       inUse=0   loc[P2]=reading   (P2's localCount = 0)   <- both read BEFORE either writes
Step 3  P1: T2       localCount(0) < LIMIT(1) -> OK, P1 moves to writing
Step 4  P2: T2       localCount(0) < LIMIT(1) -> OK, P2 moves to writing
Step 5  P1: T3       inUse' = 0 + 1 = 1        loc[P1]=holding
Step 6  P2: T3       inUse' = 0 + 1 = 1        loc[P2]=holding   <- OVERWRITES P1's update

INVARIANT VIOLATED:  PoolInvariant (inUse <= LIMIT)
  Actual state:  inUse = 1,  loc[P1] = holding,  loc[P2] = holding
  Both P1 and P2 believe they hold the pool's ONE resource. inUse says "1,"
  but two processes are using it - the counter is now permanently wrong,
  and a THIRD process reading inUse=1 will correctly assume 0 are free
  when actually 0 truly are free but for the wrong reason: two live
  holders, one accounted for.
```

*What just happened:* this is a lost update, same family as the money-transfer race in the
prerequisite guide, but a different shape - there the damage was a wrong sum; here it's a resource
pool that thinks it has more capacity than it does, or (as shown) under-counts concurrent holders
so cleanly that `inUse` looks plausible while being wrong. Step 2 is the step nobody writes a test
for. You test "one process checks out a resource." You test "the pool refuses when full." You do
not, unprompted, write a test titled "two processes both read the counter in the narrow window
before either writes it back" - because you'd have to already suspect the bug to think of the
scenario. The checker doesn't suspect anything. It tried `T1` for `P2` immediately after `T1` for
`P1` because that ordering was available, and every available ordering gets tried.

## Why a human reviewer walks past this

Code review reads top to bottom, one process at a time. `checkout()` looks correct in isolation -
read the counter, compare to the limit, increment, proceed. The bug only exists in the gap *between*
two lines, across two threads, and that gap is invisible unless you're deliberately holding both
call stacks in your head and asking "what if the scheduler pauses P1 right here?" Reviewers do this
for the one function they're told is suspicious. They don't do it for every pair of lines in every
function, because that doesn't scale to a real codebase - which is precisely the gap exhaustive
search fills.

## Where model checking still can't save you

Be precise about the boundary, because overselling this is how teams get burned later.

**The spec isn't the code.** The model above assumes `T3_write_inc` is one atomic step. If the real
implementation is `inUse = localCount + 1` compiled into multiple machine instructions with no lock
around them, the actual bug surface is *wider* than the model captures - the checker verified a
design that assumed atomicity the code might not have. You still need to verify that your
implementation's atomic operations are actually atomic (a mutex, a compare-and-swap, a language
guarantee) - that's a code-level correctness question, not a spec-level one.

**Implementation bugs live outside the model entirely.** An off-by-one in the real `LIMIT` check, a
typo that decrements the wrong variable, a memory leak that never calls `T4_release` - none of these
are design flaws the spec would ever see, because the spec doesn't contain the code. Tests and
reviews still own that territory.

**The effort has to be worth it.** Writing this pool spec, defining the invariant, and running the
checker took real, non-zero time - worthwhile for a resource pool shared across a distributed
service where a stuck or over-allocated pool means an outage. Not worthwhile for a single-threaded
CLI script, or a pool that's rebuilt fresh on every request with no shared state to race on. Model
check the component where a concurrency bug would cost you an incident; skip it where there's no
concurrency to get wrong in the first place. That judgment call - not the tooling - is the actual
skill this whole guide has been building toward.

```quiz
[
  {
    "q": "In the pool race, why does step 2 (P2 reading inUse before P1 writes back) matter?",
    "choices": [
      "It doesn't matter - the order of reads never affects the outcome",
      "Both processes read the counter's OLD value before either writes the new one, so both think there's room and both proceed",
      "It causes a crash immediately",
      "It only matters if LIMIT is greater than 1"
    ],
    "answer": 1,
    "explain": "Because both reads happen before either write, both processes base their 'is there room?' decision on the same stale value - the classic setup for a lost update."
  },
  {
    "q": "Why would a human code reviewer likely miss this bug reading checkout() top to bottom?",
    "choices": [
      "Because the code has a syntax error",
      "Because the bug lives in the gap between two lines across two concurrent threads, which reviewers don't hold in their head for every line pair in a codebase",
      "Because reviewers never check counters",
      "Because the bug only happens with more than two processes"
    ],
    "answer": 1,
    "explain": "checkout() reads correctly in isolation - the flaw only exists in an interleaving between two call stacks, which is exactly the kind of case exhaustive search catches and manual review structurally tends to skip."
  },
  {
    "q": "Which of these is a genuine limit of model checking, per this phase?",
    "choices": [
      "It can verify a design assumes an operation is atomic, but can't guarantee your actual compiled code executes that operation atomically",
      "It can only find bugs that also show up in tests",
      "It works only for resource pools, not other kinds of systems",
      "It cannot express safety properties, only liveness"
    ],
    "answer": 0,
    "explain": "The checker verifies the model's assumptions (e.g. that a step is atomic). If the real implementation doesn't honor that assumption, the gap between spec and code is a separate problem tests and reviews still have to catch."
  }
]
```