Quint: Another look at the logic of TLA+

This blogpost summarizes my work on Quint after leaving Informal Systems.

I stopped to actively develop Quint at the end of 2023, when I left Informal Systems and became independent. I am still using it, if the customers so wish. Knowing the quirks and workarounds helps me to navigate around the unpolished parts quicker.

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, I believe that the answer is positive. This became especially visible in later work on ChonkyBFT and ZKsync Governance, where Quint helped connect formal specification with day-to-day engineering practice.

Quint was developed by Shon Feder, Gabriela Moreira, Thomas Pani, Jure Kukovec, and myself. It continues to be maintained and extended at Informal Systems.