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.