Using Quint to Harden Your Specifications and Catch Hidden Bugs

The more complex the systems we build, the clearer the reality becomes: specifications are executable artifacts. They encode rules, state transitions, invariants, and constraints

Most software teams treat specifications as static documents — something written once and passed downstream. But the more complex the systems we build, the clearer the reality becomes: specifications are executable artifacts. They encode rules, state transitions, invariants, and constraints. And like any other executable artifact, they can contain bugs.

Formal tools such as Quint make this explicit. They let you write your specification as a small operational model, run it, analyze it, and verify whether it actually behaves the way you believe it should. This turns the specification from a passive description into something you can actively interrogate.

To illustrate the point, consider an apparently harmless user management flow.

The Innocent-Looking Specification

Finding a bug in an innocent-looking user management system specification:

Users sign up and are placed on a wait list. Each user is either a regular user or an admin. Admins can promote other users to admin, approve people from the wait list so they become active, and demote active users to inactive (but once inactive, they never go back to the wait list).

When an admin approves someone, the system puts that person in a “waiting for confirmation” state and sends them an email. When the person clicks the link in that email, their status becomes active.

On their first login, an active user chooses a password. On later logins, they can use their email and password to obtain a login token. Every time the system receives a command, it checks this token to confirm whether the user is logged in and whether they are an admin.

Nothing in this story looks suspicious. It mirrors countless production systems.

But here is the key question:

Does this system actually allow any user to obtain a login token?

At first glance, the answer seems like an obvious “yes.” Users are approved, they confirm their email, they log in, and they get a token. But when we translate the specification into a precise executable model, something interesting happens.

What Happens When You Model It

Quint forces us to specify exactly how each transition works and what the initial state is. In this system, users start on a wait list. To become active, they must be approved by an admin. Approval transitions them to a “waiting for confirmation” state, and confirmation transitions them to active. Only active users can log in.

So far, so good.

The problem emerges when we consider the initial state: the system starts with no users.

If there are no users, then there are no admins.
If there are no admins, nobody can approve anyone.
If nobody can be approved, nobody ever becomes active.
If nobody can become active, nobody can log in.
And if nobody can log in, nobody ever gets a token.

This is a classic bootstrap problem — structurally baked into the rules of the system.

In other words:

The specification cannot produce any tokens unless at least one admin is injected into the system by fiat.

The moment we encode the rules into Quint, the tool tells us exactly that. It proves that the “NoToken” invariant is always true when the system starts with no users. That is, across all possible executions and nondeterministic choices, the system can never reach a state where a login token exists.

The Complete Quint Model

The Quint code is:

module UserSystem {

This declares a module, which is Quint’s unit of specification. All state variables, type definitions, actions, and properties live inside this module. Think of it like a namespace containing the complete state machine definition.

Types

  type UserId = int
  type Role = Admin | Regular
  type Status = WaitList | WaitingConfirmation | Active | Inactive

These are type aliases and sum types (variants):

• UserId is an alias for int, representing user identifiers.

• Role is a sum type with two variants: Admin or Regular. Each user has exactly one role.

• Status is a sum type representing the lifecycle stages a user moves through: starting on the WaitList, transitioning to WaitingConfirmation after approval, becoming Active after email confirmation, or being demoted to Inactive.

These types serve as the domain model’s vocabulary. Quint uses them for type checking and to ensure state variables hold only valid values.

State Variables

The state variables represent the users, their roles, statuses, passwords, and tokens.

  // Registered users
  var users: Set[UserId]

  // User roles (only defined for registered)
  var role: UserId -> Role

  // Status of user in lifecycle
  var status: UserId -> Status

  // Has the user set a password?
  var hasPassword: Set[UserId]

  // Logged-in tokens
  var tokens: Set[UserId]

These state variables (declared with var) define the mutable state of the entire system. In Quint, state variables are the only things that change over time as actions execute:

• users: Set[UserId] — The set of all registered user IDs. Think of this as the primary key collection in a users table.

• role: UserId -> Role — A partial map from user ID to role. Only registered users have an entry here. This is like a dictionary or lookup table mapping IDs to their roles.

• status: UserId -> Status — A partial map tracking each user’s lifecycle status. Again, only registered users have entries.

• hasPassword: Set[UserId] — A set containing IDs of users who have set a password. Membership in this set acts like a Boolean flag per user.

• tokens: Set[UserId] — A set of user IDs with active login tokens. If a user ID is in this set, they have a valid token.

Key Quint concept: State variables represent the “database” or “memory” of your system. Every action will reference these variables in their unprimed form (current state) and update them using their primed form (users’, role’, etc.) to specify the next state.

Helpers

Helpers to check if a user is an admin or active.

  def isAdmin(u: UserId): bool =
    role.keys().contains(u) and role.get(u) == Admin

  def isActive(u: UserId): bool =
    status.keys().contains(u) and status.get(u) == Active

These are pure definitions (def), which are helper functions that compute values from the current state without modifying anything:

• isAdmin(u) returns true if user u is in the domain of the role map (role.keys().contains(u)) and their role is Admin. This checks both that the user exists and has admin privileges.

• isActive(u) returns true if user u is in the domain of the status map and their status is Active.

Key Quint concept: Pure definitions (def) never use primed variables. They’re read-only queries over the current state, useful for expressing guards and preconditions clearly. Think of them as computed properties or query methods in your domain model.

Actions

Each action represents a possible state transition in the user management system, such as registering a user, approving a user, confirming email, logging in, promoting to admin, and demoting to inactive.

  // Register → enters wait list
  action Register(u: UserId): bool = all {
    not(users.contains(u)),
    users’ = users.union(Set(u)),
    role’ = role.put(u, Regular),
    status’ = status.put(u, WaitList),
    hasPassword’ = hasPassword,
    tokens’ = tokens,
  }

This action defines the Register transition. In Quint, an action is an atomic state transition with two parts:

1. Guards (preconditions): The unprimed Boolean expressions that must be true for the action to execute. Here: not(users.contains(u)) — user u must not already be registered.

2. Effects (postconditions): The primed assignments that define the next state:

   • users’ = users.union(Set(u)) — add user u to the set of registered users

   • role’ = role.put(u, Regular) — insert u into the role map with value Regular

   • status’ = status.put(u, WaitList) — insert u into the status map with value WaitList

   • hasPassword’ = hasPassword — frame condition: passwords remain unchanged

   • tokens’ = tokens — frame condition: tokens remain unchanged

The all { ... } combinator means all conjuncts must hold simultaneously. This action is enabled only when the guard is true, and when it fires, it produces the specified next state.

Engineering analogy: Think of this as a POST /users API handler that checks whether the user already exists (guard), then inserts a new user record and sets their initial role and status (effects).

  // Admin approves → WaitingConfirmation
  action Approve(admin: UserId, u: UserId): bool = all {
    isAdmin(admin),
    users.contains(u),
    status.get(u) == WaitList,
    status’ = status.put(u, WaitingConfirmation),
    users’ = users,
    role’ = role,
    hasPassword’ = hasPassword,
    tokens’ = tokens,
  }

The Approve action models an admin approving a waitlisted user:

Guards:

• isAdmin(admin) — the acting user must be an admin

• users.contains(u) — the target user must be registered

• status.get(u) == WaitList — the target user must currently be on the waitlist

Effects:

• status’ = status.put(u, WaitingConfirmation) — update the target user’s status to WaitingConfirmation

• All other state variables are explicitly left unchanged (frame conditions)

Key Quint concept: Every action must specify the next-state value for every state variable, either by updating it or by carrying it forward unchanged. This makes the frame explicit and prevents accidental omissions.

  // User clicks email → Active
  action ConfirmEmail(u: UserId): bool = all {
    status.keys().contains(u),
    status.get(u) == WaitingConfirmation,
    status’ = status.put(u, Active),
    users’ = users,
    role’ = role,
    hasPassword’ = hasPassword,
    tokens’ = tokens,
  }

The ConfirmEmail action represents a user clicking their confirmation link:

Guards:

• status.keys().contains(u) — user must exist in the status map

• status.get(u) == WaitingConfirmation — user must be awaiting confirmation

Effects:

• status’ = status.put(u, Active) — transition user to Active status

• All other state variables unchanged (frame conditions)

This models the email confirmation flow. Once active, the user can proceed to log in.

  // First login → set password and create token
  action FirstLogin(u: UserId): bool = all {
    isActive(u),
    not(hasPassword.contains(u)),
    hasPassword’ = hasPassword.union(Set(u)),
    tokens’ = tokens.union(Set(u)),
    users’ = users,
    role’ = role,
    status’ = status,
  }

The FirstLogin action models a user’s initial login where they set their password:

Guards:

• isActive(u) — user must be active

• not(hasPassword.contains(u)) — user must not have set a password yet

Effects:

• hasPassword’ = hasPassword.union(Set(u)) — add user to the set of users with passwords

• tokens’ = tokens.union(Set(u)) — issue a login token by adding user to the tokens set

• Other state variables unchanged (frame conditions)

Key observation: This is the first point where a token can be created. The guard requires the user to be active, which depends on the entire registration → approval → confirmation flow.

  // Subsequent login → token produced again
  action Login(u: UserId): bool = all {
    isActive(u),
    hasPassword.contains(u),
    tokens’ = tokens.union(Set(u)),
    users’ = users,
    role’ = role,
    status’ = status,
    hasPassword’ = hasPassword,
  }

The Login action models returning users logging in:

Guards:

• isActive(u) — user must be active

• hasPassword.contains(u) — user must have previously set a password

Effects:

• tokens’ = tokens.union(Set(u)) — issue a token (or refresh an existing one, since sets are idempotent)

• All other state variables unchanged

This represents the standard login flow after the first login. Note that it re-adds the user to tokens, which is safe because set union is idempotent.

  // Admin promotion
  action Promote(admin: UserId, u: UserId): bool = all {
    isAdmin(admin),
    users.contains(u),
    role’ = role.put(u, Admin),
    users’ = users,
    status’ = status,
    hasPassword’ = hasPassword,
    tokens’ = tokens,
  }

The Promote action allows an admin to promote any user to admin:

Guards:

• isAdmin(admin) — the acting user must be an admin

• users.contains(u) — the target user must be registered

Effects:

• role’ = role.put(u, Admin) — update the target user’s role to Admin

• All other state variables unchanged

  // Admin demotion to inactive
  action Demote(admin: UserId, u: UserId): bool = all {
    isAdmin(admin),
    users.contains(u),
    status’ = status.put(u, Inactive),
    users’ = users,
    role’ = role,
    hasPassword’ = hasPassword,
    tokens’ = tokens,
  }

The Demote action allows an admin to demote a user to inactive status:

Guards:

• isAdmin(admin) — the acting user must be an admin

• users.contains(u) — the target user must be registered

Effects:

• status’ = status.put(u, Inactive) — change the target user’s status to Inactive

• All other state variables unchanged

Key observation: Once a user is inactive, they cannot log in (since isActive(u) would return false). The spec does not provide any action to transition from Inactive back to Active or WaitList, making this a one-way demotion.

Initial Conditions

There are two initial conditions: one with no users (which leads to the bootstrap problem) and another with a bootstrap admin user.

  // Initialize with no users (bootstrap problem)
  action initEmpty = all {
    users’ = Set(),
    role’ = Map(),
    status’ = Map(),
    hasPassword’ = Set(),
    tokens’ = Set(),
  }

This initial action defines a completely empty starting state:

• users’ starts as an empty set

• role’ and status’ start as empty maps

• hasPassword’ and tokens’ start as empty sets

Key Quint concept: Initial actions define the root nodes of all execution traces. They must specify the initial value of every state variable using primed variables only. No guards are allowed in initial actions because there is no prior state to guard against.

The bootstrap problem emerges here: If the system starts with no users, no one can perform actions that require being an admin (Approve, Promote, Demote). Therefore, the first registered user (via Register) will be a regular user on the waitlist, and they can never be approved because there are no admins to approve them.

  // Initialize with one admin user (bootstrap admin)
  action initWithAdmin = all {
    users’ = Set(0),
    role’ = Map(0 -> Admin),
    status’ = Map(0 -> Active),
    hasPassword’ = Set(0),
    tokens’ = Set(),
  }

This alternative initial action solves the bootstrap problem by starting with one admin:

• users’ = Set(0) — user 0 exists

• role’ = Map(0 -> Admin) — user 0 is an admin

• status’ = Map(0 -> Active) — user 0 is already active

• hasPassword’ = Set(0) — user 0 has set a password

• tokens’ = Set() — no tokens yet (the admin can log in to get one)

Engineering insight: This is like having a “root” or “superuser” account created during system installation. With this bootstrap admin in place, the system can now approve other users, breaking the deadlock.

  // Choose which initialization to use
  action init = initWithAdmin

This defines the actual initial action for the specification by aliasing init to initWithAdmin.

Key Quint concept: The model checker looks for an action named init to determine the initial states of the system. By switching this between initEmpty and initWithAdmin, you can test different starting configurations.

Current configuration: The spec uses initWithAdmin, meaning all traces begin with user 0 as an active admin who has set a password.

State Transitions

The step action allows for nondeterministic selection of actions to simulate the system’s behavior over time.

  action step = any {
    nondet u = oneOf(Int)
      Register(u),
    nondet admin = oneOf(Int)
      nondet u = oneOf(Int)
        Approve(admin, u),
    nondet u = oneOf(Int)
      ConfirmEmail(u),
    nondet u = oneOf(Int)
      FirstLogin(u),
    nondet u = oneOf(Int)
      Login(u),
    nondet admin = oneOf(Int)
      nondet u = oneOf(Int)
        Promote(admin, u),
    nondet admin = oneOf(Int)
      nondet u = oneOf(Int)
        Demote(admin, u),
  }

This step action defines the transition relation of the system — the set of all possible one-step evolutions from any reachable state.

Key Quint concepts:

1. any { ... }: A nondeterministic choice operator that tries each branch. At least one branch must be enabled (have its guards satisfied) for the step to succeed. The model checker explores all enabled branches, creating a branching execution tree.

2. nondet x = oneOf(SomeType): Nondeterministic binding that picks an arbitrary value from the type’s domain. Here, oneOf(Int) picks an arbitrary integer. The model checker will explore representative values (typically a bounded range in practice).

3. Structure: Each branch selects nondeterministic parameters (user IDs), then invokes the corresponding action. For example:

   • nondet u = oneOf(Int) Register(u) — try to register some arbitrary user

   • nondet admin = oneOf(Int) nondet u = oneOf(Int) Approve(admin, u) — try to have some user approve some other user

Engineering analogy: Think of step as a fuzzer that randomly chooses which API endpoint to call with which parameters, exploring all possible interleavings and parameter combinations. The model checker systematically explores this nondeterministic space to find all reachable states.

How Quint uses this: When you run quint verify, the tool uses init to generate initial states and step to generate successor states, building out the state graph until it either:

• Exhausts all reachable states (proof by exhaustion)

• Finds a state violating an invariant (counterexample)

• Hits a depth or time limit

Safety Checks

Here we state the safety checks to verify the presence or absence of tokens under different initial conditions.

  // Check if no token can ever be produced (for initEmpty)
  val NoToken = tokens.size() == 0

  // Check if eventually a token is produced (for initWithAdmin)
  val TokenProduced = tokens.size() > 0

}

These are property definitions (using val) that define Boolean predicates over the current state:

• NoToken = tokens.size() == 0 — True when no tokens exist in the system. This is an invariant intended to hold in all reachable states when using initEmpty. If the model checker finds a trace where NoToken becomes false, that’s a counterexample showing that tokens can be produced.

• TokenProduced = tokens.size() > 0 — True when at least one token exists. This is a reachability property (or “witness”) intended to be satisfied in at least one reachable state when using initWithAdmin. If the model checker cannot find any state where this is true, it means tokens are never produced.

Key Quint concept: Properties are evaluated against the state graph:

• Invariant checking: Run quint verify --invariant=NoToken to verify that NoToken holds in all reachable states. If using initEmpty, this should succeed, confirming the bootstrap problem. If using initWithAdmin, this should fail, producing a counterexample trace showing how a token is created.

• Witness checking: You can search for states satisfying TokenProduced to demonstrate that the system can produce tokens.

What Quint proves here:

1. With initEmpty: The NoToken invariant holds. No execution sequence can ever produce a token because no one can become active (bootstrap problem).

2. With initWithAdmin: The NoToken invariant is violated. The model checker finds a trace where user 0 (the bootstrap admin) executes Login(0), producing a token. Alternatively, user 0 can approve other users, who can then confirm and log in, also producing tokens.

Running the Model

Quint can be used to analyze this model and check for the presence of tokens under different initial conditions, helping to identify potential issues in the user management system specification.

To run quint, you would typically use a command like:

quint verify  UserSystem.qnt --invariant NoToken
quint verify  UserSystem.qnt --invariant TokenProduced

How these commands work:

• quint verify UserSystem.qnt --invariant NoToken — The model checker explores all reachable states starting from init and applying step repeatedly. It checks whether NoToken (i.e., tokens.size() == 0) holds in every state. If it finds a state where tokens.size() > 0, it outputs a counterexample trace showing the sequence of actions that led to token creation.

• quint verify UserSystem.qnt --invariant TokenProduced — This checks whether TokenProduced holds everywhere, which is actually the opposite of what we want. To check reachability, you’d typically negate the property or use a different tool mode. The intent here is to demonstrate that tokens can be produced.

Expected results:

1. With action init = initEmpty:

   • quint verify --invariant NoToken → Success (invariant holds). The checker confirms that no trace can produce a token, proving the bootstrap problem.

2. With action init = initWithAdmin:

   • quint verify --invariant NoToken → Failure (invariant violated). The checker returns a counterexample trace, such as:

     1. Initial state: user 0 is an active admin with password, no tokens

     2. Login(0) → user 0 logs in, tokens = {0}

     3. Final state has tokens.size() > 0, violating NoToken

This demonstrates that the bootstrap admin enables token production.

Conclusion

Use Quint to check your specifications for logical consistency and to uncover hidden issues like the bootstrap problem in user management systems. LLMs will help you actually programming in Quint, running (checking) the spec, and analyzing the output from Quint.

Summary of key Quint concepts demonstrated:

• State variables (var): Mutable state that changes across transitions

• Pure definitions (def): Read-only helpers for querying current state

• Actions: Atomic state transitions with guards (unprimed) and effects (primed)

• Initial actions: Define starting states using only primed variables

• Step action: Defines the transition relation via nondeterministic choice (any, nondet)

• Frame conditions: Explicit unchanged variables in each action

• Invariants: Boolean predicates that must hold in all reachable states

• Model checking: Systematic exploration of the state graph to verify properties or find counterexamples

By encoding the informal specification as an executable Quint model, we transformed a vague “should work” into a precise statement that can be mechanically verified. The bootstrap problem, invisible in prose, becomes immediately apparent when the model checker explores the state space.