Quint is a modern specification language that is a particularly good fit for distributed systems and blockchain protocols. It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

Quint is inspired by TLA+ but provides an alternative surface syntax for specifying systems in TLA. The most important feature of our syntax is that it is minimal and regular, making Quint an easy target for advanced developer tooling and static analysis (see our Design Principles).

The syntax also aims to be familiar to engineers:

• At the lexical level, it borrows many principles from C-like languages.
• At the syntax level, it follows a few (but not all) principles that are usually found in functional languages.
• At the semantic level, Quint extends the standard programming paradigm with non-determinism and temporal formulas, which allow designers to specify protocol environments such as networks, faults, and time concisely and clearly.

Notably, Quint comes with formal semantics built-in, thanks to its foundation in TLA and it is aligned with TLA+: it will soon be supported in the Apalache model checker.

Quint is short for Quintessence, from alchemy, which refers to the fifth element. A lot of alchemy is about transmutation and energy, and Quint makes it possible to transmute specifications into executable assets and empower ideas to become referenced artifacts.

We are preparing language and tools tutorials. Visit the Tutorials page.

Check the syntax documentation and the Reference API documentation for built-in operators.

We have written examples of several specifications in Quint. Some of them accompany a TLA+ version for comparison and learning purposes. To simplify reading, use syntax highlighting for your editor (currently, VSCode, Emacs and Vim are supported).

• Quint's core tool quint:

  • Installation

  • Manual

  • REPL

• VSCode plugin:

  We strongly encourage you to use the VSCode plugin for Quint. It provides the quickest feedback loop for your specifications, reporting informative errors as you type. Install the plugin from Visual Studio Code Marketplace.

• ADR001: Transpiler architecture
• ADR002: Error codes
• ADR003: Interface to visit Internal Representation components
• ADR004: An Effect System for Quint
• ADR005: A Type System for Quint

• quint is the package for the quint transpiler
• vscode vscode plugin

In the spirit of Lessons from Writing a Compiler, we have a roadmap, where we are implementing various transpiler passes feature-by-feature, instead of completely implementing every pass.