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 TLA Toolbox has finally been released. As announced previously, the TLA Toolbox is a full-featured IDE for writing, checking and debugging specifications in TLA+ and PlusCal. Check the Tools Section for more details.
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!
