Quint: Another look at the logic of TLA⁺

Roles in the project:

• Product Owner (2023)
• Project Lead and Principal Research Scientist (2020-2022)

I stopped to actively work on Quint in the end of 2023, when I became independent.

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.