Stephan Merz: Modeling and Developing Systems Using TLA+
My slides are available here:
[ PDF | 2up PDF ].
The definitive reference is the
TLA+ home page,
that contains links to all relevant resources around TLA+. The
Verification Challenge Problem is particularly interesting.
The specification language is introduced in depth in the book
Specifying Systems by Lamport. The first chapter are a
tutorial on TLA+ and the underlying concepts. Later chapters
introduce the TLA+ tools and provide a full reference for the
The book has been published by
it is also available for personal use from
The following document is a short
cheat sheet that
recapitulates the constructions of the TLA+ specification
TLA+ is supported by the TLA+ tool set, freely available from
It consists of a syntactic and semantic analyzer, a pretty-printer for
use with LaTeX, and most importantly, the TLA+ model checker TLC.
These tools are amply described in the TLA+ book.
Several people have used theorem provers with TLA or TLA+
has used ACL2 to verify rather substantial invariants of TLA+
specifications, described in his
(which appeared as SRC Technical Note 2001-004, December 2001).
In earlier work, I used the interactive theorem prover
Isabelle to encode TLA
(but not TLA+) and to verify TLA formulas. This work is still
included in the standard Isabelle distribution, which contains
a few examples.
Below follow a few papers for further reading. Most of these
papers are copyrighted, and they are provided here only for personal
and educational use.
The papers can be grouped into two categories: some of them are
of foundational nature, explaining the logic of TLA and TLA+.
Others contain case studies or explain practical issues important
for writing TLA+ specifications. The selection is subjective, the
widely accessible foundational papers on TLA and TLA+ are not
Papers on foundational issues
- Martín Abadi and Stephan Merz:
On TLA As A Logic
We give formal definitions of TLA's syntax and semantics,
and provide some material on proof rules and advanced concepts such
as assumption-commitment reasoning. The paper complements Lamport's
original article on TLA, but is not intended to supersede it.
© Springer-Verlag, Deductive Program Design (M. Broy, ed).
NATO ASI series F, pp. 235-272 (1996).
- Stephan Merz:
On the Logic of TLA+
This is the basis of my course at the summer school; it can also be
viewed as a continuation of the paper above for TLA+.
Computers and Informatics,
vol. 22, pp. 351-379 (2003).
on the semantics of specification formalisms, edited by
- Stephan Merz:
A More Complete TLA
I introduce a slight generalization of TLA that has a simpler
axiomatization (complete for the propositional fragment).
This is an extended version, with full proofs, of the paper that
World Congress on Formal Methods. Toulouse, France.
© Springer-Verlag, LNCS 1709, pp. 1226-1244 (1999).
Practical issues and case studies
- Leslie Lamport:
Implementing and Combining
This unpublished note (courtesy Leslie Lamport, May 2004) explains
several practical aspects in writing specifications that do not
appear in the TLA+ book.
- Stephan Merz:
TLA+ case study: a resource allocator
This note presents the allocator case study used in the course
in somewhat more detail, illustrating available verification
techniques, and describing some pitfalls to avoid when writing
formal models. It appeared as a LORIA technical report (August 2004).
The TLA+ models are available as a ZIP archive.
- Michel Charpentier:
Study on Non-blocking Atomic Commitment
In a course on program verification, Michel Charpentier used TLA+
and the TLC model checker to analyse variations on an algorithm
for distributed atomic commitment. His original Web page on this
case study is
the material is included for easy reference.
- Martín Abadi, Leslie Lamport, and Stephan Merz:
A TLA solution to the
RPC-Memory Specification Problem
In 1994, Broy and Lamport posed a benchmark problem to the formal
(see the problem statement).
This paper describes our TLA+ solution.
Parts of the formal proofs have been carried out in Isabelle and
are available in Isabelle's standard distribution.
© Springer-Verlag, LNCS 1169, pp. 21-66 (1996).
- Leslie Lamport and Stephan Merz:
Specifying and Verifying
We describe the solution of a real-time variant of the Byzantine
Generals' problem in TLA+, using refinement. Parts of the proofs
have been checked in a now obsolete encoding of TLA in the LP
© Springer-Verlag, LNCS 863, pp. 41-76 (1994).
Last modified: Mon Feb 7 19:10:28 CET 2005