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
language.
The book has been published by Addison Wesley, it is also available for personal use from Lamport's page. |

The following document is a short cheat sheet that recapitulates the constructions of the TLA+ specification language.

Several people have used theorem provers with TLA or TLA+ specifications. Carlos Pacheco has used ACL2 to verify rather substantial invariants of TLA+ specifications, described in his paper (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.

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 included here.

#### 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).

(Special Issue on the semantics of specification formalisms, edited by Dines Bjørner.) **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 appeared in

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 Specifications**- 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: Case 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 here, 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
methods community
(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 Fault-Tolerant Systems**-
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
proof assistant.

© Springer-Verlag, LNCS 863, pp. 41-76 (1994).

Stephan Merz Last modified: Mon Feb 7 19:10:28 CET 2005