Collection of Tools
This web page collects all the tools used for formal verification of Pastry.
- TLA Tools are used for command line model checking.
- TLA+ Toolbox is used as IDE for writing TLA+ models, debugging the models and conducting their proof.
- TLAPS is the TLA+ proof system, used to check the proof.
- The TLA+ Homepage contains the current versions of the tools listed above and all relevant documentations.