Quint

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.

Name origin

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.

Documentation

Tutorials 🧑‍🏫

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

Syntax 🔡

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

Examples 🎼

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).

User manuals 📘

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.

Development

Developer docs 🎸

Source code #️⃣

quint is the package for the quint transpiler
vscode vscode plugin

Roadmap ✅

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.

Language feature	Parser	Name resolution	Effects	Type checker	Simulator	To-Apalache	Tutorials
Booleans	✅	✅	✅	✅	✅	❌	✅
Integers	✅	✅	✅	✅	✅	❌	✅
if-then-else	✅	✅	✅	✅	✅	❌	❌
Operator definitions	✅	✅	✅	✅	✅	❌	❌
Modes	✅	✅	✅	✅	❌ 234	❌	❌
Sets	✅	✅	✅	✅	✅/❌ 238	❌	❌
Guess	✅	✅	✅	✅	✅	❌	❌
Maps	✅	✅	✅	✅	✅	❌	❌
Lists	✅	✅	✅	✅	✅	❌	❌
Records	✅	✅	✅	✅	✅	❌	❌
Discriminated unions	✅	✅	✅	❌ 244	❌ 233	❌	❌
Tuples	✅	✅	✅	✅	✅	❌	❌
Imports	✅	✅	✅	✅	❓	❌	❌
Module definitions	✅	✅	✅	✅	✅	❌	❌
Module instances	✅	✅	✅	✅	❌ 237	❌	❌
[Multiple files][]	❌ 8	❌	❌	❌	❌	❌	❌
Constant declarations	✅	✅	✅	✅	❌ 236	❌	❌
Variable definitions	✅	✅	✅	✅	✅	❌	❌
Assumptions	✅	✅	✅	❌	❌ 235	❌	❌
Lambdas	✅	✅	✅	✅	✅	❌	❌
Multiline disjunctions	✅	✅	✅	✅	✅	❌	❌
Multiline conjunctions	✅	✅	✅	✅	✅	❌	❌
Delayed assignment	✅	✅	✅	✅	✅	❌	❌
Invariant checking	-	-			✅	❌	❌
Higher-order definitions	✅	✅	✅	✅	❌ 221	❌	❌
Runs	✅	✅	❌	❌	✅	❌	❌
Temporal operators	✅	✅	✅	✅	non-goal	❌	❌
Fairness	✅	✅	✅	✅	non-goal	❌	❌
Unbounded quantifiers	✅	✅	❌	❌	non-goal	❌	❌
String literals, see #118	✅	✅	✅	✅	✅	❌	❌
~~uninterpreted types~~, see #118	✅	✅	❌	❌	❌	❌	❌

achamayou/quint