Quint: Development and usage of a formal specification language

After seeing many developers struggling to learn existing specification languages, we at Informal Systems decided to build our own language and tools. Almost three years later, we have a working version of Quint that we and some of our partners are using to specify software and model check properties. This tutorial will explain the basics of the Quint language, walk through the tools (from parsing to simulation/transpilation to TLA+), and highlight interesting features, like the effect checker for state updates, and challenges faced throughout the development.

Gabriela is a research engineer at Informal Systems, acting as the main developer of Quint since the start of 2022. They are also a temporary lecturer for Formal Methods at UDESC (Santa Catarina State University), from where they got a bachelor's in Computer Science and a master's in Applied Computing. Their research and interests lie in the fields of programming language design and formal methods.