This is the material for the lectures read by Igor Konnov at VTSA’23.
To follow the lecture, visit the Slides and the examples in Quint sandbox.
To experiment with the tools, please install the following:
TLA+ is a language and logic for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. At Informal Systems, we have been using TLA+ to specify and reason about the protocols and distributed applications that are running in Cosmos blockchains. Our main tool of choice for TLA+ is the symbolic model checker called Apalache. In 2023, we introduced a new specification language called Quint. This language is an alternative syntax for TLA+ that should look more familiar to engineers.
In this lecture, we demonstrate the main principles of writing specifications and checking them with Apalache. We are using examples from the blockchain industry. We also show the practical applications of the tooling provided by Apalache and Quint.