The TLA Home Page
The TLA Home Page
Last modified 3 July 2016
What is TLA?
The TLA+ Google Group
The TLA Tools
Resources for Learning About TLA
Click here to find out.
TLA+ Use at Amazon
A technical report describing TLA+ use at Amazon is available
The TLA+ Toolbox and the TLA+ Tools have been released as an open-source
project, under the MIT License. The
source code is available on
The executable files for the Toolbox are available from a new site
accessible by a link on the
Toolbox's web page.
The stand-alone versions of the TLA+ Tools can be obtained through a
new link on the
TLA+ Tools web page.
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+ 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