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.
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.
Visit the Tutorials page.
- Cheatsheet
- Reference API documentation for built-in operators
- Syntax documentation
- Frequently asked questions
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).
- 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 👷
Quick previews of the tools.
-
Quint's core tool
quint
: -
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.
- 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
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 | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
✅ | ✅ | ❌ | ❌ | ❌ | ❌ | ❌ |
Quint is developed at Informal Systems.