Quint

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 blogpost 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.