The ExTLA tutorial starts here. It assumes you write Elixir and have never written a formal specification.
Getting started is the shorter path — install, one spec, one counterexample, half an hour. This page is the other question: what is this, and why would I reach for it? It is prose, and it is the only page of the tutorial with no code on it.
The pages after it are the long path, and they are meant to be read in order: the mathematics the DSL is a notation for, the DSL as it is used, what the coverage report tells you about a verdict, temporal properties and the difference fairness makes to them, symmetry and who is responsible for it, and then the two layers that connect a specification to running code. One system runs through all of it — a lock shared by a few clients, two or three depending on what a page needs to show — and each page adds something to it.
The last three pages are the ones about your own code rather than this tutorial's: how to get from a system you already have to a specification worth checking, what to do when the state space explodes, and how to keep a specification in a project so it stays true. They are where the tutorial stops being a worked example.
Every spec in this tutorial compiles, and every verdict and output it shows is what the tool really prints: if a page says a spec verifies, it does, and if it says a counterexample is seven states long, it is. The DSL reference remains the authority on what a specification means, and these pages link to it rather than restating it.
Why verify a design at all
Tests sample. You pick inputs, or a generator picks them for you, and each run exercises one path through the system. That works well when the interesting behaviour is a function of the input — and badly when it is a function of timing, because you do not choose the interleaving. Two processes that each work perfectly can deadlock on the one ordering your test suite never produced, and the test that would have caught it passes ninety-nine times out of a hundred.
Worse, the bug is usually not in the code. It is in the design: the protocol admits a sequence of steps nobody thought about. You can find that bug by writing the code, deploying it, and waiting for the ordering to happen in production — or you can describe the design precisely enough that a machine can enumerate every ordering and tell you whether any of them is bad. That is what formal verification, in the sense this library means it, is for: finding the design bug before the code exists.
A short history, because it explains the shape of the tools
The idea that a program could be reasoned about mathematically rather than merely executed is about sixty years old, and it arrived in recognisable stages.
Assertions and proof (1960s–70s). Robert Floyd's Assigning Meanings to Programs (1967) and
C. A. R. Hoare's An Axiomatic Basis for Computer Programming (1969) established that a program
could be annotated with predicates — preconditions, postconditions, invariants — and that its
correctness could be derived. Edsger Dijkstra's work on guarded commands and predicate
transformers pushed the same idea towards deriving the program from its specification. This is the
ancestry of every assert, every contract library, and of ExTLA's Layer 1.
Temporal logic (1977). Amir Pnueli's The Temporal Logic of Programs introduced reasoning about how a program's properties evolve over time — not just "the balance is never negative" but "every request is eventually answered". Concurrency needs this: the interesting properties of a protocol are about sequences, not states.
Model checking (early 1980s). Edmund Clarke and E. Allen Emerson, and independently Jean-Pierre Queille and Joseph Sifakis, proposed something different from proof: if the system has finitely many states, enumerate them all and check the property mechanically. No human ingenuity, no induction — a decision procedure. Clarke, Emerson and Sifakis received the Turing Award for it in 2007, and it is the technique ExTLA implements.
Model checking brought its own problem, immediately: state explosion. A system with twenty boolean variables has a million states; add a process and the space multiplies. Most of the research since has been about making that tractable — symbolic representations (Randal Bryant's binary decision diagrams, 1986; Kenneth McMillan's symbolic model checking, early 1990s), partial-order reduction, symmetry reduction, abstraction, and lately SMT solvers. Every reduction ExTLA offers, and every one it refuses, is a move in this space.
Proof assistants, in parallel. Where the state space is infinite, enumeration is not available and mechanised proof is: Coq (now Rocq), Isabelle/HOL, Lean, and for TLA+ specifically TLAPS. These prove more, and cost far more human effort.
Lightweight methods (1990s–2000s). The turn that made any of this reach working engineers was the realisation that you do not need to verify the implementation to get most of the value — you verify a model of the design, small enough to check and abstract enough to write in an afternoon. Daniel Jackson's Alloy and Leslie Lamport's TLA+ are both of this kind, and the canonical demonstration is Amazon's: teams applying TLA+ to S3, DynamoDB and other services found serious bugs in designs that had already been reviewed, and said so in How Amazon Web Services Uses Formal Methods (CACM, 2015). That paper is the reason a working engineer has heard of this at all.
TLA and TLA+
TLA is the Temporal Logic of Actions, Leslie Lamport's logic for describing systems: a state is an assignment to variables, an action is a predicate relating a state to its successor, and temporal operators say how properties hold along the resulting sequences. TLA+ is the specification language built on it, with the set theory and first-order logic to write the predicates in. TLC is its model checker, PlusCal an algorithm language that compiles to TLA+, and TLAPS its proof system. Lamport received the Turing Award in 2013, for this and for the distributed-systems work — Paxos, logical clocks — that motivated it.
research/tla-plus-primer.md carries the history and philosophy
in full, with the timeline; this page will not restate it. What matters here is the design stance,
because ExTLA inherits it by being modelled on TLA+:
- Mathematics rather than programming constructs. A specification is not a program. It has no I/O, no threads, no memory model — it is a formula that a set of behaviours either satisfies or does not.
- No special constructs for concurrency. Sequential, concurrent and distributed systems are written in the same notation; concurrency is what you get when several actions are enabled at once, not a feature of the language.
- Composition by conjunction. Components combine with "and". The behaviour of the whole is the intersection of the constraints of the parts.
- Abstraction is the point. A specification says what a system does, not how, which is what keeps it short enough to check and to read.
Lamport's own summary of the philosophy: "The best language for writing specifications is mathematics."
What else exists
Formal-methods tools differ mostly in what they buy their power with. Four families are worth knowing, because the trade is different in each.
Explicit-state model checkers enumerate reachable states one at a time. TLC (for TLA+) and Spin (Gerard Holzmann's checker, taking Promela models and LTL properties) are the archetypes. Exhaustive over the model, fully automatic, and limited by state explosion — the model has to be small, which is a modelling skill rather than a tooling problem. ExTLA is of this family.
Symbolic and SMT-based checkers represent sets of states as formulas rather than enumerating them, which can cover enormous spaces — nuXmv in the hardware tradition, and Apalache for TLA+ specifically, which translates a spec into SMT constraints. They handle models an explicit checker cannot, at the cost of a translation layer and its own restrictions on what you may write.
Proof assistants verify unbounded systems, with a human supplying the induction: Coq/Rocq, Isabelle/HOL, Lean, TLAPS. They prove theorems about all parameter values rather than facts about one small configuration — for a price in effort measured in weeks rather than hours.
Bounded relational and refinement frameworks. Alloy analyses a relational model exhaustively up to a scope you choose, using a SAT solver, and is excellent at structural properties. The B method and Event-B are built around stepwise refinement from an abstract specification down to code, with the refinement obligations discharged by prover.
Beside these sit the tools that work on the implementation rather than a model: schedule explorers like Concuerror, which run real code under a controlled scheduler, and runtime verification, which checks properties as the system executes. ExTLA's Layer 1 is of the second kind, and Layer 3 drives a real GenServer against the specification — but neither controls the scheduler, so neither replaces Concuerror. Concuerror is a complement, deliberately: it finds implementation bugs where ExTLA finds design bugs.
In Elixir and Erlang
The prior-art survey is the project's survey of this ground — every tool below with its authors, status, and how it relates to ExTLA, plus the gap analysis that defines what ExTLA is for. It is the authority; this is the summary.
Working from a formal spec. Erla+ (Hristov and Bieniusa, Erlang Workshop 2024) translates PlusCal specifications into executable Erlang — spec to code, one direction. Verlixir (Neave, Imperial College) goes the other way, parsing Elixir and generating Promela for Spin — code to an external checker.
Checking real code. McErlang (Fredlund and Benac Earle) replaces the BEAM's concurrency layer to explore interleavings of real Erlang programs; mature, and unmaintained. Concuerror is active, production-ready, and requires no changes to the code under test: it re-runs your existing tests under every meaningfully different schedule, with dynamic partial-order reduction to keep that finite.
Contracts. Corsa (Erlang Workshop 2022), with stateful and message-aware contracts, plus Bond, Oath and ExContract — pre- and postconditions at the function boundary, checked at runtime.
Property-based testing. PropCheck (a PropEr wrapper, including a state-machine DSL), Makina, and StreamData in the standard library. These generate command sequences against a model — the nearest neighbour to model checking in everyday Elixir use, and the difference is sampling versus exhaustion.
Types and protocols. Dialyzer and, in recent Elixir versions, the language's own set-theoretic type system check what values flow where. ElixirST (Tabone et al., University of Malta) checks message-passing protocols statically with session types.
Where ExTLA fits
In the grand scheme: ExTLA is an explicit-state model checker for finite models of designs,
written in and driven from Elixir, with a bridge from a checked design down to a running
GenServer. It is not a theorem prover (that is TLAPS), not a schedule explorer (that is
Concuerror), it does not extract models from source (Verlixir) and it does not generate code from
specifications (Erla+). What it does that none of the above does is let an Elixir team write the
specification in Elixir, check it with mix, and then check that the GenServer they wrote
actually refines it.
In the Elixir environment, the useful question is what each tool answers:
- ExUnit — does the code do the right thing on the examples I thought of?
- StreamData / PropCheck — does a property hold over many generated inputs or command sequences? Sampling, and excellent value; it will not tell you it looked everywhere.
- Dialyzer and the type system — do the values flowing through the code fit together?
- Concuerror — does this code misbehave under some schedule the BEAM could produce?
- ElixirST — do the messages between processes follow the protocol I declared?
- ExTLA — does the design admit a behaviour that violates my invariant, or fail ever to make progress? Answered exhaustively over a finite model, before or alongside the code, and then checked against the implementation.
None of these replaces another. The one gap ExTLA fills is the design-level, exhaustive, temporal-property-bearing one — and the prior-art survey was written to establish that the gap is real.
Where to start depends on what you have. A running GenServer and a property you are nervous about: Layer 1, invariants checked on every callback, no specification needed. A protocol you are about to build: write the spec and check it — that is Getting started and the next pages here. Both, and you want them connected: Layer 3.
Sources
The two documents this page draws on both carry their own references: the survey's §Sources for the Elixir and Erlang work, and the primer's §Resources for TLA+ itself — Lamport's Specifying Systems, Hillel Wayne's Practical TLA+ and Learn TLA+, Ron Pressler's series, and the AWS paper.
Next: The mathematics of TLA.