Welcome!
Welcome to the web site for the TLA+ and PlusCal user community. This site is meant to foster communication between current and potential users of TLA+ and PlusCal. It is also a single place from which news and information about the languages and tools is disseminated.
Breaking News
The Toolbox Version 1.4.1 has been released. It provides some new editor commands–most notably, one for jumping from a region in the TLA+ translation of a PlusCal algorithm to the region of PlusCal code that generated it. It also fixes a number of bugs, including ones that occurred when TLC checked large models.
A new version of the TLA+ Proof System has also been released. Click here for information.
Site Orientation
There are four top-level sections your are most likely to use. If you are new to TLA+ and PlusCal, start with the Learning section. There’s a section for documentation. The Tools Section tells how to find and install the tools. Finally, if you want to join the TLA community, have any questions, found some mistakes or just want to contribute, then visit the Community section.
Thanks for visiting, and enjoy the site!
