TLA+ | The way to specify

There are various tools available for the TLA+ specification language and PlusCal algorithm language, as described in the TLA Tools section in more detail. These command-line tools are now integrated in a full-featured IDE, called the TLA Toolbox, for writing and debugging TLA+ specifications and PlusCal algorithms. It combines editors for specifications and TLC models with already existing TLA+ tools for syntax analysis, PlusCal translation, model checking, and pretty-printing in one application. It includes the console-based TLA+ Tools and enables the use of their whole functionality through a rich graphical user interface.

The IDE provides the following functionality with a simple graphical
interface:

• Managing specifications
• A TLA+ specification editor with features like:
  • SANY integration
  • Syntax Highlighting
  • Basic content assist
  • Error markers
• PlusCal translation
• Displaying a pretty-printed PDF version using TLATeX
• The TLC Model Checker, with:
  • A simple interface for managing models
  • A rich model editor
  • An extended TLC result display
  • A cool trace explorer
• The TLAPS proof system, with features for:
  • Viewing and editing hierarchical proofs
  • Running the prover (soon to be released)
  • Displaying the status of proofs (soon to be released)

See the TLA Toolbox page for more details.