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.

This is how typical Quint code looks:

  // `validateBalance` should only be called upon genesis state.
  pure def validateBalance(ctx: BankCtx, addr: Addr): bool = and {
    ctx.accounts.contains(addr),
    val coins = getAllBalances(ctx, addr)
    coins.keys().forall(denom => coins.get(denom) > 0),
  }

If you would like to see the same code in TLA⁺, here is how it looks:

\* `validateBalance` should only be called upon genesis state.
validateBalance(ctx, addr) ==
  /\ addr \in ctx.accounts
  /\ LET coins == getAllBalances(ctx, addr) IN
     \A denom \in DOMAIN coins:
       coins[denom] > 0

Want a preview of the tools before reading any further? Check Quick previews.

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 🧑‍🏫

Visit the Tutorials page.

Syntax 🔡

• Cheatsheet
• Reference API documentation for built-in operators
• Syntax documentation

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

Community and help

• Join the chat in the Quint zulip stream ☎️
• Join the Quint discussions 💡
• Contribute your spell to the collection of Quint spells 📜
• Contribute to the development of Quint 👷

Tools 👾

Quick previews of the tools.

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

• VSCode plugin for ITF traces by @hvanz:

  This a plugin that visualizes traces that are produced by Quint and Apalache. Install the ITF Trace Viewer from Visual Studio Code Marketplace.

Development

Developer docs 🎸

• 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
• ADR006: Design of modules and lookup tables

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.

• ✅ Completed
• 🟢 Won't get in your way, but there's still work to be done
• ❌ Not implemented yet

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