Leslie Lamport

Last modified on 2 September 2023

TLA+ Foundation   [24 April 2023]

The TLA+ Foundation, a project of the Linux Foundation, has been created.  It is an independent, non-profit organization that is henceforth responsible for determining what the TLA+ language is and will be.  It will also support the adoption of TLA+ and the development of TLA+ tools.  Click here for details.

Old TLC Liveness Bug   [22 July 2022]

We have become aware of a TLC bug that existed until May 2015 that could have caused TLC to fail to perform liveness checking without issuing any error report.  This bug was triggered by trying to check a large number of individual liveness properties.  Click here for more details.

Apalache Model Checker   [17 Mar 2022]

The new Apalache model checker for TLA+ is now available.  Click here for information.

Survey   [16 Mar 2022]

To help us get a better picture of our community, we have begun an ongoing survey of the TLA+ community.  If you have not already done so, please fill it out here.

TLA+ Conference   [16 Mar 2022]

This year's conferences will be held on 22 September 2022 in St. Louis, Missouri.

PlusCal Tutorial  [2 Dec 2021]

A new tutorial that teaches PlusCal to beginners is now avaiable here.

TLA+ Community Events  [28 Nov 2021]

The 2021 TLA+ Conference was held on 30 September in St. Louis, USA, in association with the Strange Loop conference.  A TLA+ Tutorial was given on 8 October in Freiburg, Germany, in conjunction with DISC 2021.  The programs of both events, with links to the videos and slides of most of the presentations, can be found on this web page.

Weeks of debugging can save you hours of TLA+  [7 Feb 2021]

A video by Markus Kuppe described here.

VSCode Alternative to the Toolbox   [2 Jan 2021]

A Visual Studio Code extension for TLA+ is available here.  It lacks many features of the Toolbox, but people who dislike the Toolbox may prefer to use it.