Quint is a developer-friendly (some say delightful) formal specification language based on TLA+. It comes with useful tooling for exploring models, including a random simulator and integration with the Apalache model-checker.
The project was started by Igor Konnov at Informal Systems in 2021 to test the following hypothesis:
Do engineers have an easier time onboarding to TLA+, if they are offered a syntax that looks more like a modern programming language?
In addition, Quint comes equipped with standard tools that are expected by software engineers, but uncommon for formal specification languages: a type checker, a VSCode plugin, and a testing framework.
I joined the project in 2022 at Informal Systems, contributing to various parts of the system, including
- the Quint-to-Apalache transpilation (
quint verify), - the CosmWasm smart contract spec example, and the ICS-20 (fungible token transfer) spec,
- code completion and symbol renaming for the VSCode extension,
- and many internal fixes and updates.
Quint was developed by Igor Konnov, Gabriela Moreira, Shon Feder, Jure Kukovec and myself. It is maintained and further extended at Informal Systems.