Model checking primer

Model checking is a way to explore the behaviours of a model and determine whether a property holds over all reachable behaviours. The key idea is exhaustive exploration of an abstract state space: not “one run” but all runs consistent with the model.

The method is most useful when concurrency and failure modes create many interleavings. In those settings, testing can miss rare schedules. A checker can either confirm that a property holds for the model, or produce a counterexample trace that demonstrates how the property can fail.

Quick takeaways

• It checks the model, not the codeA result is meaningful only relative to modelling assumptions.
• Counterexamples are the main outputA trace is actionable evidence: it shows a concrete sequence of steps to failure.
• Abstraction is a design decisionToo detailed explodes; too coarse hides the bug you care about.
• Safety vs liveness differSafety violations have finite witnesses; liveness needs fairness or progress assumptions.
• State explosion is realThe discipline is choosing what to model and what to abstract away.

Problem framing (why it matters)

As systems become concurrent, “correctness” becomes a property of a space of behaviours rather than a single path. Even simple protocols can fail under unusual interleavings: message reorderings, timeouts, retries, or races between updates.

Model checking is valuable precisely because it makes those interleavings explicit. Instead of relying on informal reasoning (“that should never happen”), it forces a precise statement: which states are reachable, and which properties should never be violated.

Key concepts (definitions + mini examples)

Model as a transition system

Most model checkers use some form of a transition system: a set of states, an initial state, and a relation that describes allowed transitions. You can picture it as a graph where nodes are states and edges are possible steps.

Safety vs liveness

Safety properties assert that “something bad never happens”. If safety fails, there is a finite trace that demonstrates the failure. Liveness properties assert that “something good eventually happens”. If liveness fails, the witness is often an infinite behaviour that never makes progress.

In practical work, many important requirements are safety-like: “no duplicate effects”, “no negative balance”, “no two leaders at once”. Liveness appears when you need progress under fairness assumptions: “a request eventually completes” or “a lock is eventually released”.

Abstraction

Abstraction shrinks the state space by omitting details that do not matter to the property. For example, you might abstract data values into equivalence classes (“empty” vs “non-empty”), while keeping control structure (ordering, branching) intact.

A useful rule: if you can explain why a detail does not affect the property, it is a candidate for abstraction. If you cannot, you probably need that detail.

Practical checks (steps/checklist)

1) Write the property in plain language first

Start by writing the requirement as a short sentence that could be falsified:

Never: the system records two charges for the same idempotency key.
Never: two leaders are active at the same time.
Eventually: a request that is accepted will be acknowledged.

2) Define the model boundary

Decide what is inside the model and what is environment behaviour. Environment modelling is where most mistakes happen. If your real environment includes retries and timeouts, your model must include them or explicitly rule them out.

3) Look at the counterexample as a debugging artifact

A counterexample is a trace in the model, not in the implementation. Use it as a prompt: which step corresponds to a real event, and which step is an artefact of abstraction? If the trace seems impossible, it often means the model assumptions are wrong.

4) Iterate the model deliberately

Treat modelling as refinement: start small, check key invariants, then add details only when needed. Each refinement should answer a concrete question, not satisfy a desire for realism.

Common pitfalls

• Over-constraining the environmentA model that forbids failures will “prove” properties that are irrelevant to production.
• Checking vacuous propertiesIf the interesting scenario is unreachable in the model, the property holds for the wrong reason.
• Misreading liveness resultsProgress requires fairness assumptions; otherwise a scheduler can starve actions forever.
• Modelling all data exactlyState explosion is often driven by data; abstract data when the property is about control or ordering.
• Forgetting to connect back to a boundary contractA model check helps when it validates or refines the intended interface behaviour.

Related notes

• Specs, invariants, and contractsProperties become useful when connected to explicit assumptions and guarantees.
• Session types and protocolsA way to specify and check ordering constraints in message protocols.
• Time, clocks, and orderingMany counterexamples are fundamentally about reordering and causality.
• Consensus without the hypeConsensus protocols are classic targets for model-based reasoning.