Quint

A modern and executable specification language

Executable

Quint

checked names and types

executable

English & Markdown

not checked

not executable

Abstract

Specification Languages

define only what you care about

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

Get started

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