The TLA+ project site has moved to Please go there instead.

Project Description
Tools for TLA+ specifications and PlusCal algorithms, including the Toolbox,
an IDE for writing specifications and running tools to check them.

This CodePlex site hosts the source code for the TLA+ Toolbox and TLA+ Tools.
The executable versions of the code are available for download through a link on the
TLA+ web site at,
under the same M.I.T. license with which the source code has been released.
The TLAPS proof system can be downloaded from
For information about TLA+, visit the TLA+ web site.

Last edited Nov 9 at 12:05 PM by mku, version 8