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 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 Mafra, Thomas Pani, Jure Kukovec, and myself. It is maintained and further extended at Informal Systems.