The TLA Home Page
Last modified 19 July 2018
What is TLA?
The TLA+ Google Group
The TLA Tools
Resources for Learning About TLA
Click here to find out.
If you've written rigorous correctness proofs of concurrent algorithms
described in TLA+, then you know that the key to the proof is an
inductive invariant. Finding the right inductive invariant is
hard. It should be made easier by new features added to TLC for
checking that a formula is an inductive invariant. What an
inductive invariant is and how to use TLC to check if a formula is one
are described in this document.
You can use the TLA+
to communicate with members of the TLA+ community, including the
maintainers of the tools. Post a message if you have a question, want
to report a bug, or just want to tell us what you're doing with TLA+.
The easiest way to post a message is to send email to
x should be replaced
The TLA+ tools are: the SANY parser, the TLC model checker, the
PlusCal translator, the TLATeX pretty printer, and the TLAPS proof
system. These tools are all used from the TLA
Toolbox, an IDE (integrated development environment). Downloading
the Toolbox downloads all the tools except for TLAPS, which must
be downloaded separately from
the TLAPS web site.
The tools can also be downloaded without the Toolbox to be used from a
command line, as described here (for all
tools except TLAPS).
Some limitations of the tools and some enhancements to them are
described only here.
- The TLA+
Video Course This will eventually be a series of
video lectures that explain how to write TLA+ specifications.
Now, only a few introductory lectures are available.
- The TLA+ Hyperbook
This is a work in progress that is far from complete. However, the
parts that are are written provide the best introduction to TLA+ and
the tools, as well as being a good way to get started learning
PlusCal. It also has a brief introduction to the TLAPS proof system.
- The TLA+ Book
This is a real, published book that you can download. It contains a
complete description of TLA+ and the TLC model checker at the time of
its publication. The first 90 or so pages are all that most engineers
will want to read. There have been changes to the TLA+ language since
then--the major changes being the addition of constructs for writing
proofs. These changes are described here.
Examples A somewhat random collection of example TLA+
- PlusCal See the
PlusCal web page for documents that
describe the PlusCal algorithm language.
The TLAPS web site is currently the best place to go to find out how
to use the proof system.
- Summary of TLA+ A 7-page "cheat sheet"
that compactly describes all of the TLA+ language and definitions
from the standard modules.
- Lamport's TLA Papers
This web page lists almost everything Leslie Lamport has written
about TLA. It includes some helpful introductory material.
- Other TLA Links
Links to work relevant to TLA not on the TLA+ or TLAPS web sites.
This page can be found by searching the Web for the 21-letter
Please do not put this string in any document that could wind up on
the web--including email messages and pdf and Word documents.
You can refer to it in Web documents as "the string obtained by
removing the - from