# Model checking Model checking explores every reachable state of a formal, executable model of a system and reports any violation of a stated property. A violation is a state that breaks an invariant, or a path that breaks a temporal-logic property. The model is *much smaller* than the implementation; that is what makes exhaustive exploration tractable. The technique's canonical industrial use is checking distributed protocols, where example tests cannot reach the interleavings that break the system. ## What it catches - **Concurrency bugs that survive testing.** Deep interleavings that no example test reaches. - **Protocol-level safety violations.** Two-phase commit variants, leader-election bugs, consensus violations, cache-coherence holes. - **Liveness violations.** With temporal logic (*"every accepted request is eventually applied"*), the checker finds runs where the property fails to hold. - **Spec ambiguity.** Writing the spec formally forces ambiguities into the open. AWS reports this as the largest day-to-day value of TLA+, not the bugs the model checker finds. - **Counterexamples as input to the design.** When the checker finds a trace that breaks safety, the trace itself is the bug report. By itself, model checking does **not** catch the gap between the specification and the real implementation. A verified spec the code diverges from is verified against the wrong thing. Property-based and differential testing on the same surface, and [executable-spec techniques](https://quality.stereobooster.com/executable-specifications.md), narrow that gap. [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) checks the implementation itself against assertions up to a bounded depth, and [systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) explores the same interleavings in the running program. ## Tools ### Distributed-systems flavor - **[TLA+](https://lamport.azurewebsites.net/tla/tla.html)** with the **[TLC](https://github.com/tlaplus/tlaplus)** explicit-state model checker, and **[Apalache](https://apalache-mc.org/)** (a symbolic TLA+ checker). The AWS reference toolchain (Newcombe et al. 2015; Brooker and Desai 2024)[^newcombe2015] [^brooker2024]. Used on DynamoDB and S3. - **[Alloy](https://alloytools.org/)** — relational model finder; lighter learning curve than TLA+. Used for software-architectural sketches. - **[P](https://github.com/p-org/P)** (Microsoft) — a domain-specific language (DSL) for asynchronous distributed systems; used in Azure Storage. ### Automata- and protocol-flavor - **[SPIN](https://spinroot.com/spin/whatispin.html) / [Promela](https://spinroot.com/spin/Man/promela.html)** — automata-based; used for aerospace and protocol verification. - **[NuSMV](https://nusmv.fbk.eu/) / nuXmv** — symbolic model checkers for finite-state systems; hardware and embedded protocols. - **[UPPAAL](https://uppaal.org/)** — real-time systems (timed automata). ## When to use, when not **Use:** - Distributed protocols and consensus algorithms, where a failure depends on the ordering of messages rather than on any one input. - Cache coherence, replication, leader election, gossip, recovery protocols. - Anywhere a *spec* is more valuable than a *test*: the formal spec lives longer than any implementation and survives ports. - Before implementation, not after. The cheapest model-checking bug is one fixed at the spec stage. **Don't:** - For pure business logic. The cost/benefit favors [decision tables](https://quality.stereobooster.com/decision-tables.md) and [property-based testing](https://quality.stereobooster.com/property-based-testing.md). - As a substitute for testing the implementation. Model checking verifies the spec, not the code. - On an enormous model. State-space explosion is the operative limit; if TLC takes more than a few CPU-hours, abstract the model or use the symbolic Apalache checker. - Without sustained investment in the skill. Even at AWS, where it is routine, model checking demands a steep learning curve and specialist expertise (Brooker and Desai 2024)[^brooker2024]. ## Evidence - **The DynamoDB result.** TLA+ caught a 35-step data-loss bug in DynamoDB's replication protocol that survived design review, code review, and testing (Newcombe et al. 2015)[^newcombe2015]. - **Multi-system deployment at AWS.** By 2015 the same paper reported TLA+/[PlusCal](https://lamport.azurewebsites.net/tla/pluscal.html) applied to 10 large systems across 7 teams, with named bug counts: S3's fault-tolerant low-level network algorithm (2 bugs, 804 lines PlusCal); S3 background data redistribution (1 bug + 1 in the proposed fix, 645 lines); DynamoDB replication and group-membership (3 bugs); EBS volume management (3 bugs); an internal lock manager (1 bug + verified optimization) (Newcombe et al. 2015)[^newcombe2015]. - **Cosmos DB.** A formal TLA+ specification of Cosmos DB's user-facing consistency semantics uncovered previously poorly-understood behaviors and documentation gaps, and exposed data-consistency errors in dependent Azure services; a past high-impact outage was traced to the same misunderstanding (Hackett et al. 2023)[^hackett2023]. - **Curated industrial signals.** Multiple independent teams report concrete bugs caught with TLA+: an Amazon engineer estimating TLA+ cut two months off a four-month schedule; eSpark Learning catching "several major bugs" with two days of spec work; Cockroach Labs finding a complex bug in its parallel-commit optimization, estimated at >10 hours to debug otherwise; OpenComRTOS attributing a 10× smaller codebase to specification (Wayne 2020)[^wayne2020]; these are anecdotal self-reports, not controlled measurements. ## Related **Same name, different thing — Model checking vs bounded model checking** They share a name but check different things. Model checking explores an abstract *model* or spec exhaustively against a temporal or safety property: the model is small enough to explore in full, but a passing run says nothing about whether the implementation matches it. [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) checks the *implementation itself*, unrolled to a fixed depth *k*: there is no model-fidelity gap, but the verdict holds only up to depth *k*. Model checking trades implementation-fidelity for unbounded exploration of a model; bounded model checking trades depth for checking the real code. **Exploring the program's behavior space** All explore many program behaviors; they differ in what they run and what they guarantee. Model checking works on a spec or model and is exhaustive over it. [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) runs the *actual code*, solving path constraints to reach branches a fuzzer can't, with a bounded-exhaustive verdict; [bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) runs the actual code too, but poses a single SMT query over the whole program unrolled to a fixed depth rather than exploring paths one at a time. [Fuzzing](https://quality.stereobooster.com/fuzzing.md) runs the actual code too but samples inputs empirically: cheaper per case, no exhaustiveness claim. **Model checking vs probabilistic model checking** Both check whether a property holds over a system's state space; they differ in the *kind* of property and model. Model checking checks a *boolean* temporal or safety property over a state-transition model: it holds, or there is a counterexample. [Probabilistic model checking](https://quality.stereobooster.com/probabilistic-model-checking.md) generalizes this to a *stochastic* model (a Markov chain or MDP) and a *quantitative* property, computing the probability that it holds, either exactly (PRISM, Storm) or by sampling for state spaces too large to enumerate. ## Classification - **Quality dimensions:** Reliability, Functionality. - **Area:** Distributed protocols, consensus and replication algorithms, cache coherence, concurrent state machines, hardware protocols. - **Guarantee:** Exhaustive within the model's bounds. ## Referenced by - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) · Methods - [Combinatorial and pairwise testing](https://quality.stereobooster.com/combinatorial-testing.md) · Methods - [Example tests](https://quality.stereobooster.com/example-tests.md) · Methods - [Executable specifications](https://quality.stereobooster.com/executable-specifications.md) · Methods - [Exhaustive coverage (MC/DC, MCC)](https://quality.stereobooster.com/exhaustive-coverage.md) · Methods - [Formal methods](https://quality.stereobooster.com/formal.md) · Methods - [Probabilistic model checking](https://quality.stereobooster.com/probabilistic-model-checking.md) · Methods - [Safety analysis](https://quality.stereobooster.com/safety-analysis.md) · Methods - [State machines and statecharts](https://quality.stereobooster.com/state-machines.md) · Methods - [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) · Methods - [Temporal-logic falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) · Methods - [Verifying concurrency](https://quality.stereobooster.com/concurrency.md) · Methods - [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^newcombe2015]: Newcombe, Chris, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. "[How Amazon Web Services Uses Formal Methods](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)." *Communications of the ACM* 58 (4): 66–73. . [^brooker2024]: Brooker, Marc, and Ankush Desai. 2024. "[Systems Correctness Practices at Amazon Web Services](https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/)." *Communications of the ACM*, ahead of print. . [^hackett2023]: Hackett, A. Finn, Joshua Rowe, and Markus Alexander Kuppe. 2023. "[Understanding Inconsistency in Azure Cosmos DB with TLA+](https://arxiv.org/pdf/2210.13661)." *2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)*, 1–12. . [^wayne2020]: Wayne, Hillel. 2020. *[The Business Case for Formal Methods](https://www.hillelwayne.com/post/business-case-formal-methods/)*. . ## Acronyms - DSL — domain-specific language - MC/DC — modified condition/decision coverage - MCC — multiple-condition coverage - MDP — Markov decision process - SMT — satisfiability modulo theories