Leslie Lamport

Last modified on 18 March 2022

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.

TLA+ Community Event   [3 Nov 2020]

This virtual event was held in October 2020 as a satellite of the DISC 2020 Conference.  The program and videos of the talks can be found on its Web site.

PlusPy   [6 Aug 2020]

This is a system written by Robbert Van Renesse that actually executes a TLA+ specification.  See this post on the TLA+ Google group.

New TLAPS Release   [5 Aug 2020]

After much too long, there has been a new release of the TLAPS proof system.

Community Modules   [5 Aug 2020]

This is an open GitHub repository for TLA+ users to share specifications or parts of specifications, such as operator definitions, that may be useful to others.

TLC Profiler   [5 Aug 2020]

The Toolbox provides profiling of a TLC execution of a model.  It can show you in what parts of a spec TLC is spending a lot of time, as well as helping find problems with the spec.  It's on a help page that can be found here on the web or in the Toolbox by searching help for profiling.

TLC Features   [5 Aug 2020]

The ability to collect and report information with the TLC module's TLCGet and TLCSet operators has been enhanced.  See the document Current Versions of the TLA+ Tools for details.

TLC Liveness Checking Error-Reporting Bug   [21 Apr 2020]

Because of a bug that has existed for many years, if TLC runs out of memory or another resource while checking liveness, then it produces the correct error message but exits normally, without producing an error code.  The Toolbox displays no error warning when this happens, and you have to look carefully at the Model Results page to see that TLC did not complete successfully.  When run from a command line with no options that cause TLC to produce extra output, the error message should be easy to see.  A shell script that runs TLC will probably not report the error.  This bug was fixed in the 20 April 2020 release of TLC.