Tests do not prove the absence of a bug. This does

Where the difference costs money

None of these is about the amount of code; all are about the number of combinations. That is exactly where exhaustive checking applies: protocols, state machines, locking, coordination between services. Ordinary CRUD is not in that set, and dragging model checking there is a waste.

What model checking is

You describe the system as a state machine: initial states, actions (each with a guard and an effect) and the statements that must always hold. The tool then visits every reachable state and either finds a path into a state where a statement is false, or proves that no such path exists.

const spec = {
  name: 'counter',
  processes: 2,
  init: [{ n: 0 }],
  actions: [
    {
      name: 'p0: increment',
      process: 0,
      reads: ['n'],
      writes: ['n'],
      step: (s) => (s.n < 3 ? [{ n: s.n + 1 }] : []),
    },
  ],
  invariants: [{ name: 'n stays small', reads: ['n'], holds: (s) => s.n <= 3 }],
  terminal: (s) => s.n === 3,
};

One detail of the shape matters: the guard and the effect live in one function. The action returns its successor states, and an empty list means “impossible right now”. That way the two cannot drift apart — a classic source of wrong hand-written models.

The second: reads, writes and the symmetric process sets are declared, not guessed. TLA+ asks for the same thing. The price is honest: a wrong declaration becomes a bug in the specification rather than silent unsoundness in a tool that quietly dropped the states that mattered.

The counterexample matters more than the verdict

“A violation is possible” is useless without the path to it. Breadth-first search makes the path shortest by construction, so the counterexample reads like an incident report rather than a dump.

✗ peterson (check then set) — invariant "at most one process in the critical section"

  trace
    (initial)                    pc=00 flag=00
    p0: check the other flag     pc=10 flag=00
    p1: check the other flag     pc=11 flag=00
    p0: raise flag and enter     pc=31 flag=10
    p1: raise flag and enter     pc=33 flag=11

Both look, both see a lowered flag, both walk in. Four steps, and it is obvious why the flag has to go up before the check. Things like this take a minute with a trace and weeks with “sometimes two of them end up inside”.

Why brute force does not work directly

The number of states grows as a product: six processes in five phases is 15,625 combinations, and that is a toy. So the substance of the tool is not the search but everything done to avoid searching.

The last row matters more than the first two. Where processes constantly read and write each other’s variables there is nothing to reduce — and the tool must honestly deliver nothing. That row is an assertion in the test suite: a tool that claimed a gain there would be claiming something false.

Two ways not to search

Symmetry. When processes are interchangeable, states differing only by permuting them are the same state. Six workers in five phases give 15,625 assignments but only 210 multisets: what matters is how many are where, not which one is which.

Commuting actions. When two actions touch nothing in common, the order between them is not observable: having explored one order, you learn nothing from the other. Formally these are ample sets, and their four conditions each earn their place — drop one and the checker will confidently miss violations.

How to check the thing doing the reducing

Here is the ugliest part of the whole exercise. A reduction that drops states it should have kept produces exactly the same output as one that works: “no violation found”. From inside the reduced search there is no way to tell which one you are holding.

The only workable answer is not to take the reduction at its word. The exhaustive search is kept alongside: slow, complete, and unable to be wrong. Every specification runs through both, and the reduced verdict is required to match the full one. The reduction is trusted not because its author is confident but because it agrees with something that cannot be mistaken.

That guarantee has a boundary worth naming: the comparison is only possible where the exhaustive search still runs — on small models. Precisely where the reduction is not needed. It is inherent to the approach, and it does not invalidate the check, but it sets its ceiling.

Liveness: nothing crashes, it just never gets there

Safety asks whether a bad state is reachable, and breadth-first search answers it. Liveness asks whether something good eventually happens, and it is violated by an infinite run in which it never does. In a finite state space such a run is a lasso: a path into a cycle, then the cycle forever.

The trouble is that most such cycles are absurd: they require a process that could run to simply never be scheduled. Weak fairness rules those out — a continuously enabled process must eventually move. Without that condition every concurrent program “fails” liveness and the checker is useless.

✗ spinlock — can loop forever without process 0 reaching its critical section
  The cycle is fair: process 1 keeps moving; process 0 is blocked

  then forever
    p1: acquire   pc=03 lock=1
    p1: release   pc=00 lock=-1

A spinlock is perfectly safe — two processes are never inside at once — and it starves. Peterson passes the same check, and the turn variable exists for no other reason. The difference between “safe” and “safe and makes progress” is worth being able to name: in queues, locks and distributed leases it is the source of hangs that monitoring never reports as errors.

What this method cannot do

• It checks the model, not the code. That is both the main limit and the main risk: a proven model and an implementation that drifts from it is an ordinary situation. Models catch mistakes of design, tests catch mistakes of execution; neither replaces the other.
• Reductions are sound with respect to what you declare. An action that writes an undeclared variable can cost you dropped states. It is a contract, not an analysis.
• Only invariants and one form of liveness. Statements of the form “always true” and “eventually happens” under weak fairness. No nested temporal operators, no strong fairness, no full LTL.
• Everything is in memory. Thousands or tens of thousands of states, not billions: no disk-backed store, no symbolic representation.
• For serious work there are TLC and SPIN. Decades of engineering behind them, disk-backed state storage, distributed checking, and languages designed for the job.

When it pays off on a commercial project

In money terms this pays off where wrong data costs more than downtime: financial systems, stock accounting, integrations with external providers. Neighbouring write-ups: payment idempotency and what happens to your data when the master dies.