News

News

Leslie Lamport

Last modified on 1 March 2024


Revised Draft of New TLA Book   [1 March 2024]

The preliminary draft of A Science of Concurrent Programs by Leslie Lamport has been extensively revised.  It is now the current version, available here.

Draft of New TLA Book   [2 January 2024]

A preliminary draft of a new book tentatively titled A Science of Concurrent Programs by Leslie Lamport is available here.  The book explains the scientific principles underlying the TLA+ language.  It contains a lot of math.  All the math beyond high school algebra is explained, but it will be tough going for readers who haven't taken an introductory university math class for computer science students that covers things like sets and logic.  The book contains little discussion of how TLA+ is used in practice, but it explains why TLA+ is what it is.

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.