• Stars
    star
    811
  • Rank 56,200 (Top 2 %)
  • Language
    TypeScript
  • License
    Apache License 2.0
  • Created over 3 years ago
  • Updated 15 days ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Quint

build badge Visual Studio Marketplace Version npm (scoped)

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

Tools πŸ‘Ύ

Quick previews of the tools.

  • Quint's core tool quint:

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

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 βœ… βœ… 🟒 βœ… βœ… non-goal βœ…
Temporal operators βœ… βœ… βœ… βœ… non-goal ❌ ❌
Fairness βœ… βœ… βœ… βœ… non-goal ❌ ❌
Unbounded quantifiers βœ… βœ… ❌ ❌ non-goal ❌ ❌
String literals, see #118 βœ… βœ… βœ… βœ… βœ… βœ… βœ…
uninterpreted types, see #118 βœ… βœ… ❌ ❌ ❌ ❌ ❌

More Repositories

1

tendermint-rs

Client libraries for Tendermint/CometBFT in Rust!
Rust
610
star
2

hermes

IBC Relayer in Rust
Rust
441
star
3

apalache

APALACHE: symbolic model checker for TLA+ and Quint
Scala
417
star
4

atomkraft

Advanced fuzzing via Model Based Testing for Cosmos blockchains
Python
77
star
5

cosmos.nix

A reproducible package set for Cosmos, IBC and CosmWasm
Nix
56
star
6

basecoin-rs

An example ABCI application making use of tendermint-rs and ibc-rs
Rust
55
star
7

modelator

Model-based testing tool
Python
53
star
8

tm-load-test

tm-load-test tool - Tendermint load test application
Go
46
star
9

themis-contract

A command line-based parameterized contracting tool
Go
46
star
10

unclog

Unclog your changelog
Rust
36
star
11

multisig

Painless multisig for many keys across many cosmos-sdk chains
Go
35
star
12

cross-chain-validation

TLA
33
star
13

modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Python
28
star
14

CometMock

Drop-in replacement for CometBFT in end-to-end tests
Go
25
star
15

sovereign-ibc

Implementation of IBC modules by `ibc-rs` that can run with Sovereign SDK rollups
Rust
22
star
16

tla-apalache-workshop

Material for a workshop on Apalache and TLA+. To be populated with more examples.
22
star
17

vdd

Verification-Driven Development
21
star
18

testnets

Various different test network-related configurations for Tendermint
Python
15
star
19

audits

Security Audits by Informal Systems
TLA
15
star
20

hermes-ibc-workshop

Hermes IBC Workshop - Fungible Token Transfer (ics-20) between two Starport chains
TypeScript
14
star
21

cosmwasm-to-quint

Semi-automated modelling and Model-Based Testing for CosmWasm contracts
Rust
14
star
22

gm

Tool to manage local gaiad instances - without docker
Shell
13
star
23

flex-error

Rust
13
star
24

atomkraft-cosmos

TLA
12
star
25

verification

Specifications of the protocols and the experiments on their verification
9
star
26

hermes-sdk

Rust
9
star
27

jsonatr

JSON Artifact Translator
Rust
8
star
28

apalache-tests

Benchmarks for apalache
SMT
6
star
29

context-generic-programming

Context-generic programming guide
Rust
6
star
30

gopherator

Modelator's cousin for Golang
Go
5
star
31

apalache-bench

Apalache Bench Tests
HTML
5
star
32

vscode-itf-trace-viewer

VS Code extension for viewing ITF traces
TypeScript
5
star
33

mtcs

Multilateral Trade Credit Set-off
Rust
5
star
34

itf-rs

Rust library for consuming Apalache ITF traces
Rust
5
star
35

audit-celestia

Workspace set up for collaboration in the Celestia audit
Makefile
5
star
36

ibc-starknet

Meta repository for managing IBC Starknet projects
Cairo
4
star
37

stakooler

The koolest tool for Cosmos stakers
Go
4
star
38

megablocks

Prototype to investigate an Atomic IBC solution based on Megablocks
Go
4
star
39

quint-ml-experiments

F*
4
star
40

got

Game of Tendermint
Shell
4
star
41

themis-tracer

A tool for managing complex contexts for developing critical systems
Rust
4
star
42

quint-sandbox

Material used in interactive demos and tutorials
Bluespec
3
star
43

gravity-dex-demo

Instructions to run the Gravity Dex Demo
Go
3
star
44

chainpulse

Monitoring tool for IBC relayers
Rust
3
star
45

agoric-kernel-models

TLA+ models for Agoric Swingset Kernel
TLA
3
star
46

hydro

Hydro (aka AtomWars) project repo
Rust
3
star
47

kvstore-plus-plus

KVStore++ is an ABCI application that can be used for testing with multiple CometBFT releases
Go
2
star
48

hermes-hackatom-demo

Demo for Hackatom - Hermes
TypeScript
2
star
49

cycles-sandbox

A playground for Cycles demos, experiments and prototypes.
Rust
2
star
50

apalache-chai

Chai: Client for Human-Apalache Interaction
Python
2
star
51

ics29-fee-tla

TLA
2
star
52

consumer-chain-tool

One-click Consumer Chain Tool
Go
2
star
53

sov-rollup-starter

Rust
2
star
54

itf-go

Go library for un/marshalling ITF files
Go
2
star
55

quint_awesomwasm24_workshop

Bluespec
2
star
56

merkleeyes

Go
1
star
57

OsmosisAtomkraft

Informal Systems Atomkraft adaptations and TLA specs for Osmosis audit project
TLA
1
star
58

euc

End-user computing for a better user experience
Shell
1
star
59

safe-regex

Fork of https://gitlab.com/leonhard-llc/safe-regex-rs
Rust
1
star
60

noir-ecies

Roff
1
star
61

ignite-blog

Cosmos-SDK blockchain following Ignite's Blog tutorial
TypeScript
1
star
62

economics-analysis

Economics analysis for various projects
1
star
63

ibc-proto

IBC Proto Rust implementation
Rust
1
star
64

reactor-experiments

Experiments to help us establish a concurrency architecture for Tendermint in Rust
Rust
1
star
65

cgp-workshop

Workshop materials for context-generic programming
Rust
1
star
66

partnership-heliax

Bluespec
1
star
67

cosmwasm-ibc

Facilities for implementing ibc-rs-powered light clients and applications as CosmWasm contracts.
Rust
1
star
68

hermes-sovereign-relayer

IBC Relayer for Sovereign SDK, powered by Hermes SDK
Rust
1
star