Skip to content

Software Quality

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, narrow that gap. Bounded model checking checks the implementation itself against assertions up to a bounded depth, and systematic concurrency testing explores the same interleavings in the running program.

Tools

Distributed-systems flavor

  • TLA+ with the TLC explicit-state model checker, and Apalache (a symbolic TLA+ checker). The AWS reference toolchain (Newcombe et al. 2015; Brooker and Desai 2024)1 2. Used on DynamoDB and S3.
  • Alloy — relational model finder; lighter learning curve than TLA+. Used for software-architectural sketches.
  • P (Microsoft) — a domain-specific language (DSL) for asynchronous distributed systems; used in Azure Storage.

Automata- and protocol-flavor

  • SPIN / Promela — automata-based; used for aerospace and protocol verification.
  • NuSMV / nuXmv — symbolic model checkers for finite-state systems; hardware and embedded protocols.
  • UPPAAL — 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 and property-based testing.
  • 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)2.

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)1.
  • Multi-system deployment at AWS. By 2015 the same paper reported TLA+/PlusCal 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)1.
  • 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)3.
  • 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)4; these are anecdotal self-reports, not controlled measurements.

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 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 runs the actual code, solving path constraints to reach branches a fuzzer can't, with a bounded-exhaustive verdict; bounded model checking 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 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 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

References

  1. Newcombe, Chris, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. "How Amazon Web Services Uses Formal Methods." Communications of the ACM 58 (4): 66–73. https://doi.org/10.1145/2699417. ↩↩↩

  2. Brooker, Marc, and Ankush Desai. 2024. "Systems Correctness Practices at Amazon Web Services." Communications of the ACM, ahead of print. https://doi.org/10.1145/3729175. ↩↩

  3. Hackett, A. Finn, Joshua Rowe, and Markus Alexander Kuppe. 2023. "Understanding Inconsistency in Azure Cosmos DB with TLA+." 2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), 1–12. https://doi.org/10.1109/icse-seip58684.2023.00006. ↩

  4. Wayne, Hillel. 2020. The Business Case for Formal Methods. https://www.hillelwayne.com/post/business-case-formal-methods/. ↩