Quint: Another look at the logic of TLA+
This blogpost summarizes my work on Quint after leaving Informal Systems....
I stopped to actively work on Quint in the end of 2023, when I left Informal Systems and became independent.
Roles in the project:
- Product Owner (2023)
- Project Lead and Principal Research Scientist (2020-2022)
Quint is an alternative syntax for the logic TLA+. When we started the project at Informal Systems in 2021, we wanted to test the following hypothesis:
Would engineers onboard to TLA+ faster, when they are offered a syntax that looks more like a programming language?
In short, we believe that the answer is positive. For instance, see the recent blogposts on specification and model checking of ChonkyBFT and ZKsync Governance.
In addition to the alternative syntax, Quint offers several features that are expected by software engineers:
- a type checker and an effects checker,
- a VSCode plugin,
- a testing framework and a randomized simulator.
Quint was developed by Shon Feder, Gabriela Moreira, Thomas Pani, Jure Kukovec, and myself. It is maintained and further extended at Informal Systems.