Repository files navigation

Website •Getting Started •Documentation •Community

Quint is a modern specification language that is a particularly good fit fordistributed systems, such as blockchain protocols, distributed databases, andp2p protocols. Quint combines the robust theoretical basis of theTemporalLogic of Actions (TLA) with state-of-the-art type checking anddevelopment tooling.

Here is a small specification for a bank:

module bank{/// A state variable to store the balance of each account  var balances: str-> int  pure val ADDRESSES= Set("alice","bob","charlie")action deposit(account, amount)={// Increment balance of account by amount    balances'= balances.setBy(account, curr=> curr+ amount)}action withdraw(account, amount)={// Decrement balance of account by amount    balances'= balances.setBy(account, curr=> curr- amount)}action init={// At the initial state, all balances are zero    balances'= ADDRESSES.mapBy(_=>0)}action step={// Non-deterministically pick an address and an amount    nondet account= ADDRESSES.oneOf()    nondet amount=1.to(100).oneOf()// Non-deterministically choose to either deposit or withdraw    any{      deposit(account, amount),      withdraw(account, amount),}}/// An invariant stating that all accounts should have a non-negative balance  val no_negatives= ADDRESSES.forall(addr=> balances.get(addr)>=0)}

This design lacks some important checks, and we can use the Quint CLI to find aviolation to theno_negatives property, which ideally should hold:

$ quint run bank.qnt --invariant=no_negatives

And the result is a violation where address"alice" has balance-79 in the second state.

An example execution:[State0] {balances: Map("alice"->0,"bob"->0,"charlie"->0)}[State1] {balances: Map("alice"->-79,"bob"->0,"charlie"->0)}[violation] Found an issue(45ms).Use--seed=0x1112de300ce425 to reproduce.Use--verbosity=3 to show executions.error: Invariant violated

Check theGetting Started guideto see how we can fix this problem and formally verify the result.

A simple and familiarsyntax

to support engineers reading and writing specifications

An expressivetype system

to ensure the domain model is coherent

A noveleffect system

to ensure state updates are coherent

IDE support via LSP

giving real time feedback when writing specifications

AREPL

enabling interactive exploration of specifications

Asimulator

enabling tests, trace generation, and exploration of your system

A symbolic model checker

to verify your specifications viaApalache

Quint is inspired byTLA+ (the language) but provides an alternative surfacesyntax for specifying systems in TLA (the logic). The most important feature ofour syntax is that it is minimal and regular, making Quint an easy target foradvanced developer tooling and static analysis (see ourdesignprinciples andpreviews of thetooling).

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 many principles found in functional languages.
• At the semantic level, Quint extends the standard programming paradigm withnon-determinism and temporal formulas, which allow concise specification ofprotocol environments such as networks, faults, and time.

Thanks to its foundation in TLA and its alignment with TLA+, Quint comes withformal semantics built-in.

type Status= Working| Prepared| Committed| Abortedconst ResourceManagers: Set[str]var statuses: str-> Statusaction init={  statuses'= ResourceManagers.mapBy(_=> Working)}val canCommit: bool= ResourceManagers.forall(rm=> statuses.get(rm).in(Set(Prepared, Committed)))val notCommitted: bool= ResourceManagers.forall(rm=> statuses.get(rm)!= Committed)action prepare(rm)= all{  statuses.get(rm)== Working,  statuses'= statuses.set(rm, Prepared)}

CONSTANTResourceManagersVARIABLEstatusesTCTypeOK==statuses\in[ResourceManagers->{"working","prepared","committed","aborted"}]TCInit==statuses=[rm\inResourceManagers|->"working"]canCommit==\Arm\inResourceManagers:statuses[rm]\in{"prepared","committed"}notCommitted==\Arm\inResourceManagers:statuses[rm]#"committed"Prepare(rm)==/\statuses[rm]="working"/\statuses'=[statusesEXCEPT![rm] ="prepared"]

To learn more about Quint's motivation and design philosophy, watch this15minute presentation, delivered at Gateway toCosmos in 2023.

• Join the chat in theTelegram group or in theZulip stream
• Join theQuint discussions on GitHub
• Contribute your spell to the collection of Quint spells
• Contribute to the development of Quint
• Join or co-design meetings: We hold fortnightly meetings with users and thoseinterested in contributing to the design and development of Quint. Contact us ifyou would like an invitation.

View theQuint documentation.

We aspire to have great, comprehensive documentation. At present, we have agood start, but still far to go. Please try what we have available and sharewith us any needs we have not yet been able to meet.

Quint is short for 'quintessence', from alchemy, which refers to the fifthelement. A lot of alchemy is about transmutation and energy, and Quint makes itpossible to transmute specifications into executable assets and empower ideas tobecome referenced artifacts.

Quint has been designed and developed by theApalache team:GabrielaMoreira,Igor Konnov,Jure Kukovec,Shon Feder,andThomas Pani. ❤️

Thanks for notable contributions goes toRomain Ruetschi,Philip Offtermatt,Ivan Gavran,and,Ranadeep Biswas.

Quint is developed atInformal Systems.

Supported by the Vienna Business Agency.