My TLA+ Home Page

I am the creator of TLA+, 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. 

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

Is it  TLA+  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 a Visual Studio Code extension for TLA+.

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+ .