Quint Modelling

basicSpells

Pick the flow

guidelines/from-nothing.md

guidelines/from-requirements.md

guidelines/from-code.md

guidelines/from-tlaplus.md

.qnt

guidelines/review.md

guidelines/review.md

Shared modelling spine

• Executable from the first line. Quint specs run immediately — you validate design decisions as you make them, not at the end. Never build more than one step without verifying the previous one:

  quint typecheck

  , then

  quint run

  . Typecheck is not enough — a spec can typecheck and still fail to execute, which defeats the whole point of an executable spec. The trap to watch for: a

  const

  not given a value typechecks but cannot run —

  quint run

  fails with

  Uninitialized const

  . To make the spec runnable, instantiate the const in a concrete instance module —

  module spec_3 { import spec(C = Set(1,2,3)).* }

  — and run that module. (

  assume

  documents a premise; it does not supply a value — see Step 1 and quint-lang's

  guidelines/simulations.md

  .) After each addition, actually run it — if you can't

  quint run

  the module, it isn't done. Use

  quint run

  only — never

  quint verify

  . This holds for the whole skill: building, iterating, reviewing, sanity-checking invariants — every step uses sampled

  quint run

  , not once

  quint verify

  , not even as a final pass.

  verify

  is exhaustive bounded model checking (Apalache): far slower (minutes to hours) and not part of the modeling workflow. It is a model-checking tool, documented in quint-lang (

  guidelines/cli.md

  ,

  guidelines/simulations.md

  ) — reach for it only when the user explicitly asks to model-check the spec, never on your own.
• What, not how. Model observable state transitions and their effects. Abstract away implementation detail (serialization, memory management, retry plumbing). If a detail doesn't affect an invariant you care about, it doesn't belong in the spec.

Reference examples

examples/

examples/tendermint/

choreo::

Id -> LocalState

choreo::cue

agreement

validity

const

../quint-lang/guidelines/choreo.md

examples/ewd426.qnt

step

const

temporal

var

Set[Msg]

tendermint/

choreo::

Step 1 — Separate concerns

• State machine — variables, initialization, transitions →

  var

  ,

  init

  , actions
• Functional logic — pure computations: guards, quorum checks, state updates →

  pure def

• Properties — what must always hold, what must be reachable, what must eventually happen →

  val

  invariants + witnesses, plus

  temporal

  properties for liveness (Step 5; quint-lang has the detail)

const

2 * f < n

run

assume

## Assume

run

f

n

Id -> LocalState

Step 2 — Shape the state

• How many actors → the state shape. One actor → a single

  var s: Record

  . N actors of the same kind → one

  Id -> LocalState

  map (the record describes one actor; see "Scaling to N" below). Distinct roles → either a field on

  LocalState

  (e.g.

  role: Coordinator | Participant

  ) or separate maps. Get the actor count/roles right and the shape falls out.
• How actors communicate → the message medium. Messages → a separate

  var

  for the medium, not crammed into

  LocalState

  : unordered

  Set[Message]

  soup (the default), or

  ... -> List[Message]

  ordered per-pair queues only when delivery order is load-bearing. No messages, coordination through common state → shared memory (no medium var; see

  examples/ewd426.qnt

  ). This is the "Communication shapes" choice detailed just below.
• Actors + communication → Choreo or not. Multiple actors coordinating by exchanging messages → default to Choreo (see "Default to Choreo" below). A single actor, or actors coordinating through shared state → plain Quint. So answer "who, how many, and how do they talk?" first, and all three decisions below are mostly settled before you write a type.

• Group into a record when the fields are the local state of one entity (a node's phase + log + vote), are always passed together, or an invariant relates several of them. This is the usual case.
• Keep flat (separate

  var

  s) only when the variables are genuinely independent concerns that change on their own, or the spec is small enough that grouping adds no clarity. (Some canonical examples, e.g.

  ewd840

  , keep per-field maps flat because the fields don't form an obvious unit.)

type State = {
  phase:    str,
  balances: NodeId -> int,
  members:  Set[NodeId],
}

var state: State

apply…

State

state' = applyTransfer(state, …)

LocalState

type NodeId = int
type LocalState = { phase: str, balance: int, voted: bool }

var nodes:    NodeId -> LocalState   // per-actor cohesive state
var messages: Set[Message]           // genuinely global concern → its OWN var, not inside LocalState

var state: State

var nodes: NodeId -> LocalState

can…(State, …): bool

apply…(State, …): State

can…(LocalState, …): bool

apply…(LocalState, …): LocalState

state

nodes.get(id)

state' = applyOp(state, …)

nodes' = nodes.set(id, applyOp(nodes.get(id), …))

init

NODES.mapBy(_ => <record>)

Id -> LocalState

• Message soup —

  var network: Set[Message]

  , processes receive any in-flight message. The default for asynchronous protocols; use it unless ordering genuinely matters.
• Shared memory — no message medium; processes read/write common state directly. See the bundled

  examples/ewd426.qnt

  (a token ring where each node reads its neighbours).
• Ordered per-pair queues —

  ... -> List[Message]

  with head/tail ops. Use only when delivery order is semantically required (e.g. logical-clock causality); it is more expensive to model-check than soup. The corpus spec

  LamportMutex

  is the canonical example — prefer soup unless you can name why ordering is load-bearing.

Default to Choreo for distributed protocols

choreo::cue

NodeId -> LocalState

step

LocalContext

Transition

examples/ewd426.qnt

../quint-lang/guidelines/choreo.md

examples/tendermint/

choreo::cue

agreement

validity

accountability

with_cue

tendermintTest.qnt

--main=valid

var

Step 3 — Write the functional logic (pure functions)

pure def

• Can it happen? — a

  pure def … : bool

  guard (the precondition).
• What's the resulting state? — a

  pure def … : State

  that computes the next state, assuming the guard holds.

pure def canTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): bool =
  amount > 0 and from != recipient and s.balances.get(from) >= amount

pure def applyTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): State =
  { ...s, balances: s.balances.setBy(from, b => b - amount)
                              .setBy(recipient, b => b + amount) }

Keep the guard separate from the update because they are separate facts about the operation: one says when it is allowed, the other says what it does. The action (Step 4) uses the guard to decide whether it fires at all. A single

pure def

returning

{ success, newState }

— handing back the unchanged state when the guard fails — fuses the two and pushes the action toward a no-op branch; prefer the split. (If a failed operation is itself something the system observes and reacts to, model that failure as its own guarded action, not as a fallback.)

Step 4 — Wire the state machine (guarded actions)

all { ... }

success

action init: bool = all {
  state' = { phase: "idle",
             balances: NODES.mapBy(_ => INITIAL_BALANCE),   // pre-populate every map
             members: NODES },
}

action transferAction(from: NodeId, recipient: NodeId, amount: int): bool = all {
  canTransfer(state, from, recipient, amount),          // guard — disables the action when false
  state' = applyTransfer(state, from, recipient, amount),
}

else

unchanged_all

pure def

init

.get()

Step 5 — Properties: witnesses first, then invariants

quint run --witnesses

// the state you want to be reachable — written plainly, no negation
val someBalanceChanged: bool =
  state.members.exists(n => state.balances.get(n) != INITIAL_BALANCE)

quint run spec.qnt --witnesses someBalanceChanged --max-steps 10
  → someBalanceChanged was witnessed in 90 trace(s) out of 100 explored (90.00%)

val w = not(target)

--witnesses

--witnesses

val noNegativeBalances: bool =
  state.members.forall(n => state.balances.get(n) >= 0)

quint run --invariant noNegativeBalances --witnesses someBalanceChanged

guidelines/from-requirements.md

guidelines/simulations.md

someBalanceChanged

init

var

guidelines/patterns.md

Step 6 — Compose

step

and simulate

any { ... }

action step: bool = {
  nondet from = NODES.oneOf()
  nondet dst  = NODES.oneOf()   // `dst`, not `to` (a built-in) — see quint-lang
  any {
    transferAction(from, dst, 10),
    // other actions…
  }
}

• Check witnesses with

  quint run --witnesses

  — expect a non-zero trace count (reachable); 0% means a dead action.
• Check invariants with

  quint run

  (sampled) — expect no violation; read counterexample traces step by step when one appears. Use

  quint run

  for this, not

  quint verify

  (see the "Executable from the first line" principle —

  verify

  is only for when the user explicitly asks to model-check).

A guarded model can reach a state where nothing is enabled

quint run

[ok] No violation found

--max-steps

quint verify

Found a deadlock

verify

quint run

unchanged_all

--max-steps

run

*_test.qnt

Step 7 — Self-review, then hand off the spec

• Guarded actions — no business logic in an action beyond the guard and assignments; it lives in

  pure def

  s, and the guard is lifted into the action so it's disabled when it can't fire (Step 4).
• Witness per major action — every action in

  step

  has a witness, and each one is reached in

  0 traces under

  quint run --witnesses

  , not dead at 0 traces (Step 5).

• At least one protocol-level invariant — a real safety property (no two leaders, conservation, agreement), not just a type/bounds check; and every invariant references a

  var

  .

• init

  assigns every

  var

  and every action assigns every

  var

  (a missing

  x' = x

  is a silent stutter bug); every map is pre-populated (Step 4).
• Right abstraction — IDs are opaque (no string manipulation), messages are a

  Set

  unless ordering is the property, no serialization/retry/memory detail leaked in.

guidelines/review.md

README.md

• What it covers — which modules/protocols are modelled, which assumptions (

  const

  declarations, with

  run

  -test checks for the ones that must hold) are encoded, which properties are verified.
• What it does NOT cover — implementation detail left out on purpose, edge cases excluded (and why), properties still to add. This honesty note is what stops the spec from being over-trusted.
• When to update it — for a spec that grounds an artifact (code, a TLA+ source), update the spec and re-verify before changing the artifact.

quint run

Conventions

• NodeId

  /

  LocalState

  for per-actor state, and

  NODES

  for the participant set (the

  Set[NodeId]

  the model ranges over); descriptive type names after the protocol (

  VoteRequest

  ,

  PrepareMsg

  ) not

  Msg1

  ,

  Msg2

  .
• Small domains:

  N = 3

  actors (or

  N = 2

  for first exploration) and value ranges like

  0..10

  are enough for most safety properties and keep simulation cheap. Use symbolic IDs (

  int

  or

  str

  ) for participants.
• Message soup: store sent messages in one

  Set

  and don't model delivery order unless ordering is what you're verifying.
• Abstract time: when the protocol has a notion of time or progress, model it as an integer round/epoch counter (

  round: int

  ), not wall-clock time or timer mechanics — a timeout is just the round advancing. Exception: model timing explicitly only when the timing bound itself is what you're verifying.
• Start with one action: get

  init

  + one action + one witness working before adding the rest. For N actors, model one actor first, verify, then generalize to the map — never wire up all N at once.
• Test pure functions in isolation in the REPL with hand-built states; that catches logic bugs before they get tangled into the state machine.

basicSpells