I am the creator of TLA+, a high-level language for modeling programs andsystems--especially concurrent and distributed ones.  It's based onthe idea that the best way to describe things precisely is with simplemathematics.  TLA+ and its tools are useful for eliminatingfundamental design errors, which are hard to find and expensive to correctin code. 

This web page is the home page of what used to be the TLA+ website.  TLA+ is now in the hands of theTLA+ Foundation,and this is now my personal TLA+ web site.  I have retired, and Idon't know if I will make any further changes to the site otherthan correcting errors in it.  I welcome suggestions for what modifications or additions would be worth making.  Instructionsfor contacting me are onmy home page.  Below are links to the top-level sections of this web site.

  or  TLA+ ?

An explanation of what TLA+ is all about.

Items of current interest.  Last modified on 14 May 2025.

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. There is also aVisual Studio Code extension for TLA+.

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

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

A melange of miscellaneous material mostly about TLA+ .