Quint

A modern and executable specification language

Quint helps you write precise specifications and check them automatically. Find subtle bugs before they reach production.

Get Started5‑min guide

Executable

Quint

checked names and types

executable

English & Markdown

not checked

not executable

Abstract

Quint

define only what matters

Programming Languages

define how things happen, in detail

Modern

Quint

familiar syntax

CLI and your editor

Existing Spec Languages

math-y syntax

old GUI tools

bank.qnt


/// A state variable to store the balance of each account
var balances: str -> int
 
pure val ADDRESSES = Set("alice", "bob", "charlie")
 
action withdraw(account, amount) = {
  // Decrement balance of account by amount
  // Whoops, we forgot to check for enough balance
  balances' = balances.setBy(account, curr => curr - amount)
}
 
// ...
 
/// Invariant: Account balances should never be negative
val no_negatives = ADDRESSES.forall(addr =>
  balances.get(addr) >= 0
)


$ quint run bank.qnt --invariant=no_negatives


An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> -63, "bob" -> 0, "charlie" -> 0) }
 
[violation] Found an issue (44ms).
Use --seed=0x4e85b3a53f7ef to reproduce.
Use --verbosity=3 to show executions.
error: Invariant violated