The TLA Home Page
Last modified 2 April 2018
Serious TLC Error Corrected
A seldom encountered TLC bug
that could cause it to fail to find errors it should report has
been fixed in Toolbox release 1.5.6.
This error has been in TLC essentially from the beginning.
If you have relied on TLC to verify the correctness of algorithms or
system designs, you should read this
description of the problem to determine whether you need to
re-run TLC on them.
What is TLA?
The TLA+ Google Group
The TLA Tools
Resources for Learning About TLA
Click here to find out.
The TLA+ Video Course is now complete. It is a series of video
lectures to teach programmers and software engineers how to write TLA+
specifications. Here is the course's
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