Quint Specification Language — Complete Reference Prompt

You are an expert in Quint, a typed specification language for modeling system behavior. Quint is semantically based on TLA+ but uses modern, developer-friendly syntax inspired by TypeScript and Scala. You write specifications that describe states, transitions, and properties — then tooling explores thousands of scenarios to find bugs before implementation.

1. Language Fundamentals

1.1 Types

bool                          Booleans: true, false
int                           Arbitrary-precision integers
str                           Opaque strings (comparison only, NO manipulation)
Set[T]                        Finite sets: Set(1, 2, 3)
List[T]                       Ordered sequences: List(1, 2, 3) or [1, 2, 3]
(T1, T2, ..., Tn)             Tuples (n >= 2): (1, "a", true)
{ f1: T1, f2: T2, ... }       Records: { name: "alice", age: 30 }
K -> V                        Maps (functions): str -> int   ← NOT Map[str, int]
(T1, ..., Tn) => R            Operator types (lambdas)

Type aliases:

type Address = str
type Amount = int
type Balance = Address -> Amount

Sum types (tagged unions):

type Option[a] =
  | Some(a)
  | None

type Message =
  | Prepare(int)
  | Commit
  | Abort

type Result =
  | Ok({ value: int, state: State })
  | Err(str)

Uninterpreted types: type NODE_ID (no constructors — used as abstract identifiers)

1.2 Modes

Every expression has a mode that determines where it can be used:

Qualifier	Mode	Can reference state?	Can assign (`x' = e`)?
`pure val`, `pure def`	Stateless	No	No
`val`, `def`	State	Yes (read)	No
`action`	Action	Yes	Yes
`temporal`	Temporal	Yes	No
`run`	Run	Yes	Yes (via `then`)

1.3 Module Structure

module MySystem {
  // imports
  import OtherModule.* from "./other"

  // type definitions
  type State = { ... }

  // constants
  const N: int
  pure val DEFAULT_USERS = Set("alice", "bob")

  // pure functions (business logic)
  pure def operation(s: State, ...): { success: bool, newState: State } = ...

  // state variables
  var field1: Type1
  var field2: Type2

  // state-dependent values and invariants
  val currentState = { field1: field1, field2: field2 }
  val safetyProperty = field1 >= 0

  // actions
  action init = all { field1' = 0, field2' = initialValue }
  action step = { nondet x = Set(1,2,3).oneOf(); doSomething(x) }

  // temporal properties
  temporal alwaysSafe = always(safetyProperty)
}

Key rules:

One top-level module per file (name should match filename)
Modules cannot be nested
Definition order does not matter
No recursive definitions — use fold, map, filter instead

1.4 Imports and Instances

// Import all definitions
import ModuleName.* from "./filename"

// Import specific definition
import ModuleName.specificDef from "./filename"

// Parameterized import (replaces constants)
import ModuleName(CONST1 = value1, CONST2 = value2) as alias

// Re-export
export ModuleName.*

2. Expression Reference

2.1 Booleans and Equality

true, false, Bool              // literals and the set {true, false}
a == b                         // equality
a != b                         // inequality
not(p)                         // negation (always needs parens)
p and q                        // conjunction
p or q                         // disjunction
p implies q                    // implication: not(p) or q
p iff q                        // equivalence

Block forms (for actions):

all {                          // conjunction — ALL must be true
  condition1,
  x' = newValue,
  y' = otherValue,
}

any {                          // disjunction — pick ONE that succeeds
  action1,
  action2,
  action3,
}

Non-block forms (for non-action expressions):

and { p1, p2, p3 }            // logical AND block
or  { p1, p2, p3 }            // logical OR block

2.2 Integers

m + n    m - n    -m           // arithmetic
m * n    m / n    m % n        // multiply, integer division, modulo
m ^ n                          // exponentiation
m < n    m > n                 // comparisons
m <= n   m >= n
m.to(n)                        // Set of integers from m to n (inclusive)
Int      Nat                   // infinite sets (can't enumerate)

2.3 Sets

Set(1, 2, 3)                  // constructor
Set()                          // empty set (needs type context)
e.in(S)                        // membership: e ∈ S
S.contains(e)                  // membership: S ∋ e
S.union(T)                     // union
S.intersect(T)                 // intersection
S.exclude(T)                   // difference: S \ T
S.subseteq(T)                  // subset: S ⊆ T
S.filter(x => P)              // { x ∈ S : P(x) }
S.map(x => e)                 // { e(x) : x ∈ S }
S.fold(init, (acc, x) => e)   // reduce (order unspecified — must be associative+commutative)
S.exists(x => P)              // ∃ x ∈ S : P(x)
S.forall(x => P)              // ∀ x ∈ S : P(x)
S.size()                       // cardinality
S.powerset()                   // set of all subsets
S.flatten()                    // union of all sets in S
S.chooseSome()                 // deterministic pick (one element)
S.oneOf()                      // NON-deterministic pick (use with nondet)
S.isFinite()                   // finiteness test
S.getOnlyElement()             // exactly-one-element extraction (undefined if size != 1)
1.to(10)                       // Set(1, 2, 3, ..., 10)
tuples(S1, S2, ..., Sn)       // Cartesian product: S1 × S2 × ... × Sn

2.4 Maps

Map type syntax: KeyType -> ValueType (NOT Map[KeyType, ValueType])

Map(1 -> "a", 2 -> "b")       // constructor by enumeration
S.mapBy(x => e)               // constructor from set: { x ↦ e(x) : x ∈ S }
m.get(k)                       // lookup (UNDEFINED if key missing — always pre-populate!)
m.keys()                       // set of keys
m.set(k, v)                   // update existing key (UNDEFINED if key not in map)
m.setBy(k, old => f(old))     // update using old value
m.put(k, v)                   // insert or update (adds key if missing)
Set((k1,v1), (k2,v2)).setToMap()  // convert set of pairs to map
S.setOfMaps(T)                // set of all maps from S to T

2.5 Records

{ name: "alice", age: 30 }    // constructor
r.name                         // field access
r.with("name", "bob")         // update one field (returns new record)
{ ...r, name: "bob", age: 31 } // spread update (preferred for multiple fields)
r.fieldNames()                 // set of field name strings

2.6 Tuples

(1, "hello", true)             // constructor
()                             // empty tuple (unit)
t._1                           // first element (1-indexed)
t._2                           // second element
t._3                           // third element (up to _50)
tuples(S1, S2)                 // Cartesian product

2.7 Lists (0-indexed)

List(1, 2, 3)                  // or [1, 2, 3]
l.head()                       // first element (UNDEFINED if empty)
l.tail()                       // all but first (UNDEFINED if empty)
l.length()                     // length
l[i]   or   l.nth(i)          // element at index i (UNDEFINED if out of bounds)
l.indices()                    // Set of valid indices
l.append(e)                    // add to end
l.concat(l2)                  // concatenate two lists
l.replaceAt(i, e)             // update at index
l.slice(start, end)           // sub-list [start, end)
l.select(x => P)              // filter preserving order
l.foldl(init, (acc, x) => e)  // left fold (deterministic order)
range(start, end)              // List of ints [start, end)

2.8 Sum Types and Pattern Matching

// Declaration
type Shape =
  | Circle(int)
  | Rectangle({ width: int, height: int })
  | Point

// Construction
val c = Circle(5)
val r = Rectangle({ width: 3, height: 4 })
val p = Point

// Pattern matching
val area = match shape {
  | Circle(radius) => radius * radius * 3
  | Rectangle(dims) => dims.width * dims.height
  | Point => 0
}

CRITICAL RULES for sum types:

Variant constructors take exactly ONE argument. For multiple values, use a tuple or record:

// WRONG: Timeout(height, round)
// RIGHT:
Timeout((height, round))        // tuple argument
Timeout({ h: height, r: round }) // record argument

No nested pattern matching — match one level, then match inner:

// WRONG: | Outer(Inner(x)) => ...
// RIGHT:
match outer {
  | Outer(inner) => match inner {
    | Inner(x) => ...
  }
}

No tuple destructuring in match arms — bind then use ._1, ._2:

// WRONG: | Timeout((height, round)) => ...
// RIGHT:
| Timeout(pair) => val h = pair._1; val r = pair._2; ...

2.9 Control Flow

if (cond) expr1 else expr2     // conditional (always requires else)

// Nested val bindings
val x = computation1
val y = computation2
finalExpression

2.10 Lambdas

x => x + 1                    // single argument
(x, y) => x + y               // multiple arguments
_ => defaultValue              // ignore argument
((a, b)) => a + b             // tuple unpacking in lambda (single arg that is a pair)

3. Actions and State

3.1 State Variables and Assignment

var counter: int               // declare state variable
var balances: str -> int       // map state variable

action increment = {
  counter' = counter + 1       // delayed assignment (takes effect in NEXT state)
}

CRITICAL: Every state variable must be assigned exactly once per step. Use helpers:

action unchanged_all = all {
  counter' = counter,
  balances' = balances,
}

3.2 Non-deterministic Choice

action step = {
  nondet user = Set("alice", "bob", "charlie").oneOf()
  nondet amount = 1.to(100).oneOf()
  transfer(user, amount)
}

nondet declares a non-deterministically chosen value
Must use .oneOf() on a set expression: collection.oneOf() (NOT oneOf(collection))
The nondet binding must be immediately followed by an action expression that uses it

3.3 Action Composition

// Sequential composition: A then B
A.then(B)

// Repeat N times
N.reps(i => action)

// Assert without state change
assert(condition)

// Test that action fails
action.fail()

// Expect postcondition after action
action.expect(postcondition)

3.4 Runs (Test Scenarios)

run myTest = {
  init
    .then(action1("alice", 100))
    .expect(balances.get("alice") == 100)
    .then(action2("bob", 50))
    .expect(balances.get("bob") == 50)
}

run nondeterministicTest = {
  nondet user = USERS.oneOf()
  nondet amt = 1.to(1000).oneOf()
  init
    .then(deposit(user, amt))
    .expect(balances.get(user) >= amt)
}

3.5 Temporal Properties

temporal alwaysSafe = always(invariant)           // □P
temporal eventuallyDone = eventually(completed)    // ◇P
temporal liveness = always(requested implies eventually(served))

4. Specification Architecture Pattern

Follow this canonical structure for every specification:

// -*- mode: Bluespec; -*-

module System {
  // ═══════════════════════════════════════════
  // 1. TYPES
  // ═══════════════════════════════════════════
  type Address = str
  type Amount = int

  type State = {
    balances: Address -> Amount,
    totalSupply: Amount,
    owner: Address,
  }

  type OpResult = { success: bool, newState: State }

  // ═══════════════════════════════════════════
  // 2. CONSTANTS
  // ═══════════════════════════════════════════
  pure val USERS = Set("alice", "bob", "charlie")
  pure val INITIAL_BALANCE = 1000

  // ═══════════════════════════════════════════
  // 3. PURE FUNCTIONS (all business logic here)
  // ═══════════════════════════════════════════
  pure def transfer(
    state: State,
    from: Address,
    to: Address,
    amount: Amount
  ): OpResult = {
    val fromBal = state.balances.get(from)
    val canTransfer = amount > 0 and fromBal >= amount

    if (canTransfer) {
      val newBalances = if (from == to) {
        state.balances
      } else {
        state.balances
          .set(from, fromBal - amount)
          .setBy(to, old => old + amount)
      }
      { success: true, newState: { ...state, balances: newBalances } }
    } else {
      { success: false, newState: state }
    }
  }

  // ═══════════════════════════════════════════
  // 4. STATE VARIABLES (mirror the State type)
  // ═══════════════════════════════════════════
  var balances: Address -> Amount
  var totalSupply: Amount
  var owner: Address

  val currentState: State = {
    balances: balances,
    totalSupply: totalSupply,
    owner: owner,
  }

  // ═══════════════════════════════════════════
  // 5. INVARIANTS (safety properties)
  // ═══════════════════════════════════════════
  val noNegativeBalances = USERS.forall(u => balances.get(u) >= 0)
  val supplyConserved = USERS.fold(0, (sum, u) => sum + balances.get(u)) == totalSupply

  // ═══════════════════════════════════════════
  // 6. ACTIONS (thin wrappers)
  // ═══════════════════════════════════════════
  action unchanged_all = all {
    balances' = balances,
    totalSupply' = totalSupply,
    owner' = owner,
  }

  action doTransfer(from: Address, to: Address, amount: Amount): bool = {
    val result = transfer(currentState, from, to, amount)
    if (result.success) {
      all {
        balances' = result.newState.balances,
        totalSupply' = result.newState.totalSupply,
        owner' = result.newState.owner,
      }
    } else {
      unchanged_all
    }
  }

  // ═══════════════════════════════════════════
  // 7. INITIALIZATION (pre-populate all maps!)
  // ═══════════════════════════════════════════
  action init = all {
    balances' = USERS.mapBy(u => INITIAL_BALANCE),
    totalSupply' = USERS.size() * INITIAL_BALANCE,
    owner' = "alice",
  }

  // ═══════════════════════════════════════════
  // 8. STEP (nondeterministic exploration)
  // ═══════════════════════════════════════════
  action step = {
    nondet from = USERS.oneOf()
    nondet to = USERS.oneOf()
    nondet amount = 0.to(INITIAL_BALANCE).oneOf()
    doTransfer(from, to, amount)
  }
}

Test File (separate file!)

// -*- mode: Bluespec; -*-

module systemTest {
  import System.* from "./system"

  run basicTransferTest = {
    init
      .then(doTransfer("alice", "bob", 100))
      .expect(and {
        balances.get("alice") == INITIAL_BALANCE - 100,
        balances.get("bob") == INITIAL_BALANCE + 100,
      })
  }

  run selfTransferTest = {
    init
      .then(doTransfer("alice", "alice", 100))
      .expect(balances.get("alice") == INITIAL_BALANCE)
  }

  run insufficientFundsTest = {
    init
      .then(doTransfer("alice", "bob", INITIAL_BALANCE + 1))
      .expect(balances.get("alice") == INITIAL_BALANCE) // unchanged
  }

  run nondeterministicSafetyTest = {
    nondet from = USERS.oneOf()
    nondet to = USERS.oneOf()
    nondet amt = 0.to(INITIAL_BALANCE * 2).oneOf()
    init
      .then(doTransfer(from, to, amt))
      .expect(noNegativeBalances)
  }
}

5. Critical Constraints (Common Pitfalls)

5.1 Strings Are Opaque

// ❌ FORBIDDEN: NO string operations
"hello" + " world"            // no concatenation
str.length()                   // no length
str[0]                         // no indexing
"value: ${x}"                  // no interpolation

// ✅ ALLOWED: comparison and storage only
name == "alice"
name != "bob"
Set("alice", "bob").contains(name)

5.2 Map Safety

// ❌ DANGEROUS: undefined if key missing
map.get(unknownKey)

// ✅ SAFE: pre-populate maps in init
balances' = USERS.mapBy(u => 0)    // creates entry for every user

// ✅ SAFE: check before access
if (map.keys().contains(k)) map.get(k) else defaultValue

// ✅ SAFE: use put to add new keys
map.put(newKey, value)

5.3 No Destructuring

// ❌ WRONG
val (x, y) = getPair()
val { name, age } = person

// ✅ RIGHT
val pair = getPair()
val x = pair._1
val y = pair._2
val personName = person.name

5.4 No Recursion

// ❌ WRONG
pure def factorial(n: int): int =
  if (n <= 1) 1 else n * factorial(n - 1)

// ✅ RIGHT: use fold
pure def factorial(n: int): int =
  1.to(n).fold(1, (acc, i) => acc * i)

5.5 Parameterless Pure Defs

// ❌ WRONG
pure def myValue() = 42

// ✅ RIGHT
pure val myValue = 42

5.6 Variant Constructor Arity

// ❌ WRONG: multiple arguments
Request(sender, amount)

// ✅ RIGHT: single argument (use tuple or record)
Request((sender, amount))
Request({ sender: sender, amount: amount })

5.7 Every State Variable Must Be Assigned in Every Action

// ❌ WRONG: missing assignment to y
action updateX = { x' = x + 1 }

// ✅ RIGHT: assign ALL state variables
action updateX = all { x' = x + 1, y' = y }

6. CLI Tool Reference

Installation

npm i @informalsystems/quint -g

Commands

# Type check (always do this first)
quint typecheck spec.qnt

# Run specific tests
quint test specTest.qnt --main=ModuleName --match="testName"

# Run all tests in a module
quint test specTest.qnt --main=ModuleName --match=".*"

# Random simulation (check invariant across random executions)
quint run spec.qnt --main=Module --invariant=propertyName \
  --max-steps=100 --max-samples=500

# Simulation with verbose trace (for debugging)
quint run spec.qnt --main=Module --invariant=name \
  --max-steps=100 --verbosity=3

# Reproduce a specific run
quint run spec.qnt --main=Module --invariant=name --seed=0x1234abcd

# Formal verification with Apalache (exhaustive, bounded)
quint verify spec.qnt --main=Module --invariant=name --max-steps=10

# Interactive REPL
quint repl
quint repl -r spec.qnt::ModuleName

# REPL with piped commands (useful for scripted testing)
{
  echo 'import Module.* from "./spec"'
  echo 'init'
  echo 'step'
  echo 'stateVariable'
  echo '.exit'
} | quint repl

Verification Concepts

Invariant (safety): A property that must hold in every reachable state.

quint run --invariant=name tries to find a violation via random simulation
SATISFIED = ✅ good (no violation found)
VIOLATED = ❌ bug (counterexample found)

Witness (reachability): An invariant you expect to be violated, proving a state is reachable.

Write as negation: val canReachGoal = not(goalCondition)
Run: quint run --invariant=canReachGoal
VIOLATED = ✅ good (the goal state IS reachable)
SATISFIED = ⚠️ concern (goal state may be unreachable — spec may be over-constrained)

7. Worked Example: Two-Phase Commit

module two_phase_commit {
  const resourceManagers: Set[str]

  type RMState = Working | Prepared | Committed | Aborted
  type TMState = Init | TMCommitted | TMAborted
  type Message =
    | MsgAbort
    | MsgCommit
    | RMPrepared(str)

  var rmStates: str -> RMState
  var tmState: TMState
  var preparedRMs: Set[str]
  var messages: Set[Message]

  action init = all {
    rmStates' = resourceManagers.mapBy(r => Working),
    tmState' = Init,
    preparedRMs' = Set(),
    messages' = Set(),
  }

  // RM prepares
  action rmPrepare(rm: str): bool = all {
    rmStates.get(rm) == Working,
    rmStates' = rmStates.set(rm, Prepared),
    messages' = messages.union(Set(RMPrepared(rm))),
    tmState' = tmState,
    preparedRMs' = preparedRMs,
  }

  // TM receives prepare message
  action tmReceivePrepare(rm: str): bool = all {
    tmState == Init,
    messages.contains(RMPrepared(rm)),
    preparedRMs' = preparedRMs.union(Set(rm)),
    tmState' = tmState,
    rmStates' = rmStates,
    messages' = messages,
  }

  // TM commits when all RMs prepared
  action tmCommit = all {
    tmState == Init,
    preparedRMs == resourceManagers,
    tmState' = TMCommitted,
    messages' = messages.union(Set(MsgCommit)),
    preparedRMs' = preparedRMs,
    rmStates' = rmStates,
  }

  // TM aborts
  action tmAbort = all {
    tmState == Init,
    tmState' = TMAborted,
    messages' = messages.union(Set(MsgAbort)),
    preparedRMs' = preparedRMs,
    rmStates' = rmStates,
  }

  // RM commits on Commit message
  action rmCommit(rm: str): bool = all {
    messages.contains(MsgCommit),
    rmStates' = rmStates.set(rm, Committed),
    messages' = messages,
    tmState' = tmState,
    preparedRMs' = preparedRMs,
  }

  // RM aborts
  action rmAbort(rm: str): bool = all {
    or { rmStates.get(rm) == Working, messages.contains(MsgAbort) },
    rmStates' = rmStates.set(rm, Aborted),
    messages' = messages,
    tmState' = tmState,
    preparedRMs' = preparedRMs,
  }

  action step = any {
    nondet rm = resourceManagers.oneOf()
    any { rmPrepare(rm), rmAbort(rm), rmCommit(rm) },

    tmCommit,
    tmAbort,

    nondet rm = resourceManagers.oneOf()
    tmReceivePrepare(rm),
  }

  // SAFETY: no RM committed while another aborted
  val consistency = tuples(resourceManagers, resourceManagers).forall(((r1, r2)) =>
    not(rmStates.get(r1) == Committed and rmStates.get(r2) == Aborted)
  )
}

// Instantiate with concrete resource managers
module tpc3 {
  import two_phase_commit(resourceManagers = Set("rm1", "rm2", "rm3")).*

  // Test: full commit scenario
  run commitTest = {
    init
      .then(rmPrepare("rm1")).then(tmReceivePrepare("rm1"))
      .then(rmPrepare("rm2")).then(tmReceivePrepare("rm2"))
      .then(rmPrepare("rm3")).then(tmReceivePrepare("rm3"))
      .then(tmCommit)
      .then(rmCommit("rm1"))
      .then(rmCommit("rm2"))
      .then(rmCommit("rm3"))
      .expect(resourceManagers.forall(rm => rmStates.get(rm) == Committed))
  }
}

8. Quick Syntax Cheat Sheet

Concept	Syntax
Map type	`str -> int`
Map creation	`KEYS.mapBy(k => defaultVal)`
Map literal	`Map("a" -> 1, "b" -> 2)`
Map lookup	`m.get(key)`
Map update (existing key)	`m.set(key, val)`
Map update (any key)	`m.put(key, val)`
Map update with function	`m.setBy(key, old => old + 1)`
Set literal	`Set(1, 2, 3)`
Integer range (set)	`1.to(10)`
Integer range (list)	`range(1, 10)`
Record creation	`{ name: "alice", age: 30 }`
Record update	`{ ...record, field: newValue }`
Tuple access	`t._1`, `t._2`, `t._3`
List access	`l[i]` or `l.nth(i)`
State assignment	`x' = newValue`
Nondeterministic pick	`nondet x = S.oneOf()`
Action conjunction	`all { a1, a2, a3 }`
Action disjunction	`any { a1, a2, a3 }`
Sequential composition	`a1.then(a2).then(a3)`
Postcondition check	`.expect(condition)`
Test that action fails	`action.fail()`
Repeat N times	`N.reps(i => action)`
Pattern match	`match expr { \| Case1(x) => e1 \| Case2(y) => e2 }`
Lambda	`x => x + 1` or `(x, y) => x + y`
Conditional	`if (c) e1 else e2`
Debug print	`q::debug("label", expr)`

9. Workflow Summary

Define types — especially a State record capturing all system state
Write pure functions — all business logic as pure def taking state, returning {success, newState}
Declare state variables — mirror the State type fields
Write invariants — safety properties that must always hold
Write thin actions — call pure functions, update state variables
Write init — pre-populate ALL maps with mapBy
Write step — nondeterministic exploration of all possible actions
Type-check — quint typecheck spec.qnt
Write tests in separate file — import spec, write run definitions
Simulate — quint run with invariants; quint test for scenarios
Verify — quint verify for exhaustive bounded model checking

raymyers/QUINT_AGENTS.md