Model Checking in Practice

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 specifies a mutual-exclusion lock end to end - state, transitions, a safety property, and a liveness property.
Want the mechanics of checking? Phase 2 covers how a checker actually walks a state graph, and the state explosion problem - honestly.
Want to see it catch something real? Phase 3 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

Writing a Real Spec - a mutual-exclusion lock, specified completely: states, transitions, a named safety property, and a named liveness property.
Exhaustive State-Space Exploration - 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.
A Real Concurrency Bug, Caught Before Code
- a classic lost-update interleaving, the counterexample that finds it, and the honest limits of the whole approach.

Prerequisite: Formal Methods and Specification - especially its states/transitions/invariants phase (Phase 2) and its checking phase (Phase 3). Also builds on What Logic Actually Is and Predicate Logic and Quantifiers.

Phase 1: Writing a Real Spec →