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. The checker explores deep interleavings that no example test reaches.
  • Protocol-level safety violations. Two-phase-commit variants, leader election, consensus and cache coherence each carry an invariant, and the checker reports any reachable state that breaks it.
  • 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.
  • 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). AWS applied TLA+ and TLC to DynamoDB and S3 (Newcombe et al. 2015)1.
  • Alloy — relational model finder, used for software-architectural sketches.
  • P (Microsoft) — a domain-specific language (DSL) for asynchronous distributed systems. AWS used it to validate the protocol changes behind S3's move to strong read-after-write consistency (Brooker and Desai 2024)2.

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, where a failure depends on the ordering of messages rather than on any one input: consensus, replication, leader election, gossip, cache coherence and recovery.
  • 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; when TLC cannot exhaust the model, the options are abstracting it or switching to the symbolic Apalache checker.
  • Without sustained investment in the skill. The primary barriers to industrial adoption of formal-methods tools are their steep learning curve and the specialized domain expertise they require (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's replication-and-reconfiguration algorithm (1 bug + verified optimization) (Newcombe et al. 2015)1.
  • Cosmos DB. A TLA+ specification of Cosmos DB's user-facing consistency semantics documented behaviors that were poorly understood outside the Cosmos DB team, a gap that had caused data-consistency errors in dependent Microsoft products. The model also raised documentation issues, since corrected, and explained the root cause of a past high-impact outage in another Azure service (Hackett et al. 2023)3.
  • Curated industrial signals. A collection of TLA+ case reports includes 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/. ↩