Last modified on Mon 24 April 2023 at 16:23:57 PST by lamport -->
[24 April 2023]
The TLA+ Foundation, a project of the Linux Foundation, has been
created. It is an independent, non-proit 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.
[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
[16 Mar 2022]
This year's conferences will be held on 22 September 2022 in St.
Tutorial [2 Dec 2021]
A new tutorial that teaches PlusCal to beginners is now
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
VSCode Alternative to the Toolbox
[2 Jan 2021]
A Visual Studio Code extension for TLA+ is available
It lacks many features of the Toolbox, but people who dislike the
Toolbox may prefer to use it.