The TLA Toolbox

Last modified 19 July 2018


What is the Toolbox? Installing and Running the Toolbox If You Find a Problem Downloading the Toolbox Release History

What is the Toolbox?

The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools.  You can use it to:

Installing and Running the Toolbox

To install the Toolbox, you will need a Java runtime.  (You will need version 1.8.)  Just download the .zip file for your system by clicking on the appropriate link below and unzip it in a convenient location.  This will install a directory containing an executable file named toolbox (or toolbox.exe on Windows).  To run the Toolbox, just execute that file. 

The instructions that appear on the welcome screen tell you what to do next: namely, read the indicated help page.  For now, the help pages are the only user manual that exists for the Toolbox.  Read it.  Even after using the Toolbox for a while, you're unlikely to have discovered all its features.  Read all the help pages.  You never know what you might find in them.

The help pages tell you how to use the Toolbox, and they tell you most of what you need to know about the tools--especially the TLC model checker and the pretty-printer.  However, they don't describe the TLA+ and PlusCal languages.  To learn about them, see the Resources section of the TLA+ home page.

If You Find a Problem

The Toolbox works well for us.  However, there are a number of minor bugs that haven't yet been fixed.  The current bug repository, where you can look for known bugs and report new ones, is:

    The GitHub Repository tlaplus Issues page

Bugs from before 2013, including many that were considered not worth the trouble of fixing, are in:

    The Bugzilla Database

Implementing the Toolbox has involved a lot of work--mainly by Simon Zambrovski, Dan Ricketts, and Markus Kuppe.  They were able to build a sophisticated tool in a short time by using Eclipse.  However, this required compromises, and there are some annoying (but not serious) inconveniences in the Toolbox because they either didn't have the time or the Eclipse expertise to fix them.  They have also not had time to do extensive testing, which is hard and time-consuming for this type of graphical interface program.  So, please try to be helpful instead of angry if something doesn't work right.  Report the problem if it's not already in the bug list, and help us fix it if you can.  Thanks.

Downloading the Toolbox

Below is a link to a page from which you can download the versions of the Toolbox for various systems, the name of the file indicating which system it is for.  For example,  is for 64-bit Linux.  Please thank Microsoft and HP for the open-source release of the code by reading the following agreement.

By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license.   Read the license.

You can download the Toolbox from either of these sites:


Release History

Version 1.5.7 of 18 July 2018    [details]
- 32-bit versions of the Toolbox are no longer available.
- Bugs in the TLC implementation of the standard Bags module have been corrected.
- An experimental standard module Randomization, described
here, has been added.
- Numerous improvements have been made to TLC and the Toolbox.

Version 1.5.6 of 30 January 2018    [details]
- Corrects the TLC bug described
- Fixes a bug in the Toolbox's update mechanism that would cause it to make TLC impossible to run.
- Fixes a TLC bug that caused it to stop with an integer overflow exception after many hours of model checking.

Version 1.5.5 of 5 January 2018    [details]
- Provides only a partial fix of the TLC bug fixed in version 1.5.6.

Version 1.5.4 of Approximately 7 October 2017    [details]
- All known issues with Java9 and macOS High Sierra have been fixed.
- The Toolbox can now display a visual representation of a small state graph.
- TLC's error reporting has been improved.
- A number of features have been added and bugs have been fixed in the Toolbox and TLC.

Version 1.5.3 of 14 April 2017    [details]
- Bug fixes include eliminating incorrect error traces in TLC liveness checking.
- Execution by multiple worker threads in TLC has been speeded up.
- The Toolbox can now be set as the default program for running .tla files.
- The built-in PDF viewer is now the default on Windows and Linux.
- TLC can be run on multiple EC2 or Azure instances by button pushing.
- An apt repository is provided for Linux installations.

Version 1.5.2 of 21 December 2015    [details]
- Added a quick access dialog for showing and selecting models and modules.
- The toolbox now maintains backups of previous versions of modules.
- Models now have a field for free-form comments.
- Only one Toolbox instance can now be run at a time.
- A -userFile parameter allows redirecting Print/PrintT output to a file.
- Not all states of very long error traces are displayed initially.
- Ended support for 32-bit Toolbox releases on Mac OSX.
- Several optimizations and bug fixes were made.

Version 1.5.1 of 1 June 2015    [details]
- Fixes several bugs in TLC and a bug in the Toolbox's trace explorer

Version 1.5.0 of 11 May 2015    [details]
- Distributed TLC in the Cloud--significantly improves distributed TLC.
- Significantly speeds ups TLC's liveness checking.
- Improvements to the
Decompose Proof Command.
- Improvements to the TLC Errors view, including ability to show trace
   in reverse order.
- Has some changes to the way the Toolbox handles its subwindows.
- Fixes all known bugs in TLC's liveness checking.
- Fixes TLC bug of infinite looping if a recursively defined operator is used
   as an operator argument in its own definition.
- Numerous bug fixes.

Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft