The current version of the TLA+ language contains several features not described in Specifying Systems. Chief among them are constructs for writing hierarchically structured proofs. The differences between the current and previous versions of TLA, including the proof language, are described here.
The Toolbox aids reading and writing hierarchically structured TLA+ proofs by providing commands to view just the part of the structure that you want to see. These commands are described in the subtopic Viewing and Editing Structured Proofs.
TLAPS, the TLA+ Proof System, can be used to mechanically check TLA+ proofs. You can select the parts of a proof to be checked, and you can have the Toolbox display which steps' proofs have and have not been checked. The Running TLAPS subtopic describes how to run it from the Toolbox. But before you can run TLAPS, you must install it on your computer. Instructions for doing this, as well as an explanation of how to use TLAPS, on the TLAPS web page. As described on that page, if you are using Windows, you will also have to install Cygwin on your computer.
When using TLAPS, you will need to use the module TLAPS.tla and perhaps other
TLAPS library modules. The TLAPS download page will tell you in what
folder (directory) those modules are. The
TLA+ Preferences page will allow
you to declare that modules from that folder should be usable in your specifications.