Tools for TLA+ specifications and PlusCal algorithms, including the Toolbox, an IDE for writing specifications and running tools to check them.
The goal of this project is to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. We believe this can significantly improve the design process:
- Specification forces a careful and rigorous examination of what an algorithm or system should do, separate from how it should do it.
- Verification can catch bugs in an algorithm or a system design even before it is implemented, where one wants to catch and correct it.
As systems get more complex and their high-level designs become a more significant source of errors, this work will become increasingly important.