The TLA+ Home Page

The TLA+ Home Page

Leslie Lamport

Last modified on 6 December 2018

You'll miss a lot on this web site unless you enable Javascript in your browser.
This is the home page of the TLA+ web site.  TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.  It's based on the idea that the best way to describe things precisely is with simple mathematics.  TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.  The following are the top-level pages of the web site.
Is it  TLA+  or  TLA+ ?

High-Level View

An explanation of what TLA+ is all about.


Items of current interest.  Last modified on 3 January 2019.

Industrial Use

Some examples of how TLA+ has been used in industry.

Learning TLA+

Resources for learning how to use TLA+, including an introductory video course.

The Toolbox

An integrated development environment (IDE) for TLA+ and its tools.

The Tools

Tools for checking TLA+ models. The primary ones are the TLC model checker and the TLAPS proof system.

Advanced Topics

For those who know enough about TLA+ to be able to read simple specifications.

More Stuff

A melange of miscellaneous material mostly about TLA+ .