Stephan Merz: Modeling and Developing Systems Using TLA+

General reference

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.

Tools

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.

Some papers

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