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+ ?
An explanation of what TLA+ is all about.
Items of current interest. Last modified on 3 January 2019.
Some examples of how TLA+ has been used in industry.
Resources for learning how to use TLA+, including an introductory video course.
An integrated development environment (IDE) for TLA+ and its tools.
Tools for checking TLA+ models. The primary ones are the TLC model checker and the TLAPS proof system.
For those who know enough about TLA+ to be able to read simple specifications.
A melange of miscellaneous material mostly about TLA+ .