cloudparts

Formal methods

Describe a system’s design, or its code, in a precise mathematical language, then let a tool check every possible behaviour, or prove a property for all of them, instead of trying a few by hand.

1 technology on this page ↓

How it works

You write a specification: the system’s state (a counter, the log on each replica, the messages in flight), its initial states, and the steps that can change it, such as a client sending a write, a node crashing or a message arriving late. Alongside it you state the properties the design must keep. Safety properties say something bad never happens (“never two leaders in one term”, “no acknowledged write is lost”); liveness properties say something good eventually happens (“every request is eventually answered”). Then a tool checks the specification against the properties, in one of a few ways. An explicit-state model checker such as TLC enumerates every reachable state of a small, finite instance (three nodes, two values, at most four messages) and either reports that the property holds for that instance or prints a counterexample: the exact sequence of steps that breaks it. Symbolic and bounded checkers such as Apalache and the Alloy Analyzer hand the problem to an SMT or SAT solver, which copes with large data domains but looks only up to a given depth or scope. A proof system such as TLAPS or Lean proves a property for every size and every execution, but a person has to write the proof, usually around an inductive invariant. Verification-aware languages such as Dafny go one step further and check the program itself, then compile it to C#, Java, Go, Python or JavaScript. Most cloud and database teams use the lightweight end of this range: they model only the tricky part, the replication or reconfiguration protocol rather than the whole service, at the level of the design, and model-check small instances. AWS engineers described it as “exhaustively testable pseudo-code”. The catch is that the tool checks the model, not your code: a design proven correct can still be implemented wrongly, and the model is only as right as its assumptions about the network, clocks and storage. Teams narrow that gap with trace validation, replaying logs from tests or production against the specification (PObserve does this for P), and with ordinary testing, simulation and fault injection.

Think of it as

A chess engine analysing an endgame. Instead of playing a few games from the position and hoping, it looks at every legal sequence of moves and either shows that you can’t lose or gives you the exact line that loses. But it only knows the board you set up: put a piece on the wrong square and its verdict is about a different game.

Reach for it when

  • Concurrent and distributed protocols whose bugs need a rare interleaving of messages, crashes and retries: replication, leader election, reconfiguration, distributed transactions, cache invalidation, lock-free data structures
  • Before building a protocol, or before an optimisation to one already in production, when you need to know the faster version is still safe
  • Pinning down guarantees other people build on, the way Azure Cosmos DB publishes TLA+ specifications of its five consistency levels
  • Small, critical cores worth proving outright, such as an authorisation engine: AWS models Cedar in Lean, proves its security properties and tests the Rust code against the model

Think twice when

  • Code whose risk lies in business rules, user interfaces or integrations rather than concurrency and failure; tests and types catch those bugs for far less effort
  • Treating a passing model check as proof the service works: it covers the model, not the code, and only the instance sizes you configured
  • Specifications nobody will keep in step with the system; Datadog notes that keeping its models current is tedious, so routine changes rely on unit, integration and chaos tests
  • Modelling every field and message at once: the number of states grows exponentially until the checker never finishes, so abstract away everything the property doesn’t depend on

A real example

Two workers each add 1 to a shared counter by reading it and then writing back the value plus one. Code review passes, and the unit tests pass because they run one worker at a time. A short TLA+ specification models each worker as two steps, read and write, and states one invariant: once both workers are done, the counter is 2. TLC explores every interleaving and reports that the invariant is violated, with a four-step trace: worker 1 reads 0, worker 2 reads 0, and both write 1. The team switches the design to a compare-and-set that retries when the value has changed, models that version, and TLC finds no violation for two workers or for three. The specification says nothing about whether the Go code really retries; a test for that still has to be written.

Technologies

Specific products, and what each does differently.

What each provider calls it

AWS
No service checks your designs, but AWS teams have used TLA+ since 2011 and P (open source, MIT) on S3, EBS, DynamoDB, Aurora, EC2 and others. Customers meet automated reasoning inside products: IAM Access Analyzer uses logic-based reasoning on resource policies, and Amazon Bedrock Guardrails has Automated Reasoning checks (generally available since August 2025) that test model answers against a formalised policy
Google Cloud
No formal methods service; Google engineers used TLA+ and the TLAPS prover to verify a concurrent union-find data structure deployed for clustering tens of billions of data points
Azure
No formal methods service; TLA+, its proof system and Dafny grew up at Microsoft Research, and Azure Cosmos DB publishes its TLA+ consistency specifications on GitHub under MIT
Open source & others
TLA+ (MIT) with the TLC and Apalache model checkers and the TLAPS prover; P (MIT) for systems of communicating state machines; Alloy 6 for relational models; Lean 4 (Apache 2.0) for proofs; Dafny (MIT) for verified code. Jepsen, by contrast, is testing: it runs the real database under injected faults and checks the recorded history

Four ways to check#

They trade coverage against effort. Most teams start with the first and add the others only where the risk justifies them.

ApproachWhat you getWhat it costsExamples
Explicit-state model checkingEvery reachable state of a small, finite instance, and a step-by-step counterexample when a property failsSays nothing about larger instances; the state count explodes as you add nodes, values and messagesTLC for TLA+, the P checker
Symbolic or bounded checkingAll behaviours up to a depth or scope, solved by SAT or SMT, including large data domains such as integersBounded runs say nothing beyond the bound unless you also check an inductive invariantApalache for TLA+, the Alloy Analyzer
Machine-checked proofA property proved for every size and every executionA person writes the proof, which takes far longer than a model check and needs a strong invariantTLAPS, Lean, Isabelle (a TLAPS back end)
Verified code and trace checkingThe program, not just a model, meets its specification, or real runs are checked against the modelCode written in a verifying language, or logging that maps code events onto specification stepsDafny, Cedar’s Lean model with differential tests of its Rust code, PObserve for P

Formal methods, testing and chaos engineering#

Testing and fault injection run the real code, so they catch implementation bugs, but only along the paths they happen to exercise. Jepsen, for example, sets up a real cluster, sends operations from several clients while a “nemesis” injects faults, records when each operation started and ended, and checks that history against the consistency the system claims. Model checking is the reverse: it explores every interleaving, but of a model someone wrote.

Teams that rely on formal methods use both. Datadog designed Courier, its multi-tenant message queue on FoundationDB, by checking a TLA+ model with TLC (5,515,710 distinct states), then running a SimPy simulation for throughput and a chaos test in staging for node loss; its engineers note that models and simulations “do not validate its implementation”. AWS’s 2025 account of its practice lists TLA+ and P beside property-based testing, fault injection and deterministic simulation.

In code · text

---------------------------- MODULE Counter ----------------------------
\* Two workers each add 1 to x by reading it, then writing back x + 1.
EXTENDS Naturals
VARIABLES x, pc, tmp
Workers == {1, 2}

Init == /\ x = 0
        /\ pc = [w \in Workers |-> "read"]
        /\ tmp = [w \in Workers |-> 0]

Read(w) == /\ pc[w] = "read"
           /\ tmp' = [tmp EXCEPT ![w] = x]
           /\ pc' = [pc EXCEPT ![w] = "write"]
           /\ UNCHANGED x

Write(w) == /\ pc[w] = "write"
            /\ x' = tmp[w] + 1
            /\ pc' = [pc EXCEPT ![w] = "done"]
            /\ UNCHANGED tmp

Next == \E w \in Workers : Read(w) \/ Write(w)
Spec == Init /\ [][Next]_<<x, pc, tmp>>

\* The property: once both workers are done, x is 2
BothCounted == (\A w \in Workers : pc[w] = "done") => x = 2
=========================================================================
\* Counter.cfg holds two lines:  SPECIFICATION Spec  and  INVARIANT BothCounted
\* TLC reports that BothCounted is violated, with the trace
\* 1 reads 0, 2 reads 0, 1 writes 1, 2 writes 1

Often confused with

Automated testingChaos engineeringLinters, formatters and type checkers
Where it came from1994–2025

For decades formal methods had a reputation in industry, as the AWS engineers later put it, for “requiring a huge amount of training and effort to verify a tiny piece of relatively straightforward code”. Leslie Lamport took a different route for concurrent systems: his Temporal Logic of Actions (1994) describes a system as a set of allowed steps, and TLA+, with Yuan Yu’s TLC model checker (1999) and the book Specifying Systems (2002), made such specifications checkable by machine. Hardware teams came first: DEC/Compaq engineers verified cache-coherence protocols for Alpha processors in TLA+, and an Intel team found “hundreds of bugs before RTL” in a cache-coherence design.

Cloud services brought it into software. In 2011 Chris Newcombe at AWS, unhappy with bugs that survived reviews and tests, read Pamela Zave’s analysis of the Chord protocol in Alloy, tried Alloy, then chose the more expressive TLA+. By September 2014 AWS had used it on 10 large systems, including S3, DynamoDB and EBS; in DynamoDB the model checker found a data-loss bug whose shortest trace had 35 steps. Engineers learned it in two to three weeks, and the 2015 paper “How Amazon Web Services Uses Formal Methods” in Communications of the ACM argued that the reputation for poor return on investment was “quite wrong”.

Others followed and published: Azure Cosmos DB put TLA+ specifications of its consistency levels on GitHub in 2018, MongoDB has modelled its replication, reconfiguration and transactions since about 2015, Oracle Cloud Infrastructure since 2015, and Datadog described its Courier queue in 2024. AWS widened its toolkit to P, Dafny and Lean, as Marc Brooker and Ankush Desai described in Communications of the ACM in 2025, and the Linux Foundation launched the TLA+ Foundation in 2023 to fund the language’s tools.

Why it’s built this way

Check the design, not the code
AWS wanted to verify that code implements its high-level specification but knew of no tools “that can handle distributed systems as large and complex as those we are building”, so it model-checked designs, where the subtle bugs were.
Exhaustive checks of small instances
A model checker can’t enumerate an unbounded system, but it can cover every interleaving of a few nodes and messages, which is where AWS found bugs that had passed design reviews, code reviews and testing.
Plain mathematics instead of a programming language
Lamport’s view is that “the best way to describe things precisely is with simple mathematics”, which lets a specification leave out everything but the idea being checked.
Pseudocode front ends for engineers
AWS avoided the words “formal”, “verification” and “proof” at first, and found engineers often more productive starting in PlusCal, TLA+’s pseudocode-like language; P models systems as the communicating state machines engineers already draw.

Timeline

  1. 1994

    Lamport publishes “The Temporal Logic of Actions” in ACM TOPLAS

  2. 1999

    TLC, the TLA+ model checker by Yuan Yu, Panagiotis Manolios and Lamport

  3. 2002

    Specifying Systems, the TLA+ book, is published

  4. 2011

    AWS engineers start using TLA+

  5. 2015

    “How Amazon Web Services Uses Formal Methods” appears in Communications of the ACM

  6. 2018

    Azure Cosmos DB publishes TLA+ specifications of its consistency levels

  7. 2023

    The Linux Foundation launches the TLA+ Foundation on April 21

  8. 2025

    “Systems Correctness Practices at Amazon Web Services” describes TLA+, P and simulation at AWS

Sources18

Improve this page on GitHub