quint-co/quint/quint-modeling

Quint Modelling

Produce a Quint specification from whatever the user starts with. This skill owns the shared modelling discipline (below) and routes to a flow-specific guideline for the intake — the part that turns a particular kind of input into the understanding the shared steps build on.

For language syntax, operators, the CLI, and basicSpells, defer to the quint-lang reference. This skill is about how to model, not Quint syntax.

Pick the flow

Identify what the user is starting from, then read the matching guideline. The guideline handles intake — extracting the system's state, operations, and assumptions from that source. After intake, everyone converges on the Shared modelling spine below.

The first four are build flows: intake → the Shared modelling spine below. The review flow is different — there is no new model to produce; you audit an existing spec against a checklist and report findings. It does not use the spine; read guidelines/review.md and follow it directly.

If the starting point is ambiguous (e.g. "a design doc with some pseudocode"), ask the user which source is authoritative before picking — the intake differs materially.

Shared modelling spine

Every flow lands here. Intake (flow-specific) produces an understanding of the system: its entities, the operations they perform, the state each operation reads and writes, and the system-model assumptions (communication, failures, time, participants). The spine turns that understanding into a verified Quint spec.

Two principles hold throughout:

• 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

Two complete, runnable specs are bundled in examples/, one for each of the two ways components coordinate — by passing messages or by sharing state. Almost any system maps onto one of them; pick by that question, not by domain label, and read the closer match as a worked instance of the spine patterns (Step 2 state-shaping, Step 4 guarded actions, Step 5 witnesses + invariants) — to see how the pieces compose into a whole spec. (They are canonical shapes to learn from, not the only valid ones.)

If a system has both (e.g. message-passing nodes that also touch a shared ledger), start from tendermint (the message-passing structure dominates) and add shared state as its own var, per Step 2. Plain message soup (Set[Msg]) without the Choreo framework isn't a separate file — Choreo's broadcast is soup underneath, so tendermint/ is also the reference for that shape (read the state decls + a guarded transition; the choreo:: wrapper is the only added layer).

Step 1 — Separate concerns

Partition the understanding into three layers. Keeping them apart is what makes a spec testable; mixing them is the most common source of untestable specs.

• 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)

Also pin down the system-model assumptions — they shape every invariant built on top. Encode them as `const` declarations. To actually check an assumption (e.g. a quorum condition like 2 * f < n), write a `run` test that asserts it — the assume keyword documents a premise but is not enforced, so don't rely on it as a check (see quint-lang's ## Assume for why and the run-test pattern). Each flow's intake fills this in from its own source (interview, requirements doc, code, or TLA+); the checklist is the same regardless:

If an assumption is wrong, every property built on it is wrong — surface them before building.

Step 2 — Shape the state

Start from the two questions you answered in Step 1 — *who the actors are* and *how they communicate*. Together they drive every structural decision this step makes. They are not just background; they pick the shape, the message medium, and the framework:

• 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 cohesive state into a record and let the functional layer operate on that record — this is the recommended shape, because most of the time the variables that describe one entity are cohesive, and grouping keeps the functional layer clean and the invariants readable. Keeping variables flat is the deliberate exception, not a co-equal default:

• 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.)

The cohesive case — one unit:

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

The apply… pure functions take and return State; actions assign the next-state record directly (state' = applyTransfer(state, …)). No per-field reassembly.

Scaling to N instances — when there are N actors, the record describes one actor's local state, and the variable becomes a map keyed by actor id. The pure functions are unchanged — they still operate on a single LocalState; only the wiring around them changes:

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