Quint
A modern and executable specification language
Executable
Quint
checked names and types
executable
English & Markdown
not checked
not executuable
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
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_negativesAn 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