Quint Lang

Quint Lang (or just 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.

If you are impatient, here is a 15 minute intro to Quint at Gateway to Cosmos 2023.

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 🔡

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
Editor support:

We strongly encourage you to configure your editor for Quint. Our language server provides the quickest feedback loop for your specifications, reporting informative errors as you type. These are instuctions for the currently supported editors:
- VSCode: Install the plugin from Visual Studio Code Marketplace.
- Emacs: Setup two custom packages from the emacs folder.
- Vim/Neovim: Follow configuration instructions from the vim folder
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.
Writing literate executable specifications

This is a technique for embedding formal quint formal specifications inside of markdown files.

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.

✅ 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	✅	✅	✅	✅	✅	✅	❌
Tuples	✅	✅	✅	✅	✅	✅	✅
Sum types	✅	✅	✅	✅	✅	❌ 1034	❌
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	✅	✅	🟢	✅	✅	non-goal	✅
Temporal operators	✅	✅	✅	✅	non-goal	✅	❌
Fairness	✅	✅	✅	✅	non-goal	✅	❌
Unbounded quantifiers	✅	✅	❌	❌	non-goal	❌	❌
String literals, see #118	✅	✅	✅	✅	✅	✅	✅
~~uninterpreted types~~, see #118	✅	✅	❌	❌	❌	❌	❌

Quint is developed at Informal Systems.

With additional funding from
.

romac/quint