Quint for TypeScript developers

Quint is a language for describing how a system moves from state to state, plus tools that check every order in which those moves can happen. It is built on TLA+, the method AWS and Microsoft use for distributed systems, but with a syntax that reads more like TypeScript.

Quint describes a system as state, steps and “must never happen” rules, and checks every order in which the steps can run. It has its own language and checks the model, not the real code. The model is a separate, much smaller file with only the state and steps that matter, so bugs are easier to see. The cost is a second file to keep in sync with the code; the replay test in Step 5 does that.

Dafny and Lean prove that one function is right for every input. Quint answers a different question: what happens when several things run at the same time, in every possible order? This page shows how to use it next to a normal TypeScript project, with one small example: a search box. No math background needed.

Write the model as plain text, let an agent turn it into Quint, let Quint find the order that shows the wrong results, then replay its traces against the real TS code.

Why you would want this

The test passes, but a late reply for “rea” can replace the results for “react”.

A search box asks the server for results on every input:

src/search.ts

export function createSearch(fetchResults: (query: string) => Promise<string[]>) {
  const state = { query: '', results: [] as string[] };

  async function onInput(query: string): Promise<void> {
    state.query = query;
    const results = await fetchResults(query);
    state.results = results;
  }

  return { state, onInput };
}

src/search.test.ts

test('shows results for what you typed', async () => {
  const search = createSearch(async (query) => [`results for ${query}`]);
  await search.onInput('rea');
  await search.onInput('react');
  expect(search.state.results).toEqual(['results for react']);
});

The test passes. It waits for each reply before typing again. A real user doesn’t: they type “rea”, then “react”, and both requests are in flight at once. If the reply for “rea” is slower, it arrives last. The box says “react” and the list shows results for “rea”. The test never tries that order. Quint tries all of them.

When Quint fits

• Several things can happen in any order: replies, user input, workers, retries, queues, timeouts, locks.
• The bug you worry about is about order: “what if the reply for A comes back after the reply for B?”
• The rule can be said as “this must never happen”: never stale results on screen, never charged twice, never a lost message.

Quint is not the tool for proving one function’s math right for every input. See the Dafny and Lean pages for that.

Install

quint verify also needs Java 17 or newer.

npm i -g @informalsystems/quint

quint verify needs Java 17+.

Architecture

What runs underneath each quint command:

So Quint is a friendlier front end on the TLA+ toolchain, not a replacement for it. It is also why only the model check in CI needs Java.

What Quint leaves out of TLA+

Quint covers what you need to find races. Good to know:

• “It always ends” rules need --backend tlc.
• With TLC, a stuck state is not reported as an error.
• No reuse of existing .tla specs, and no proofs.

If you need those, use TLA+ directly.

Step 1: write the model as plain text (you and AI)

A markdown file next to the code: variables, actions with a guard and an effect, and the rule. You and the agent write it together.

Before any Quint, write down what the code does in a plain text file in the repo. There are concepts to learn, but no new syntax: variables and the values they can take, actions with a guard (when the step can happen) and an effect (what changes), and the rule that must hold. Write it together with a coding agent: it drafts from the TS code and asks what is unclear, you decide what the steps and rules are and correct every line. It is the file reviewers read.

Concepts: state, variables, actions, guards, effects, invariants.

quint/search.md

# Search box - spec

The user types "rea", then "react". Each query sends a request, and the replies come
back in any order. The checkable version is search.qnt, next to this file.

## Constants

- queries = "rea", "react" (typed in this order)

## Variables

- typed: 0..2 = 0 (how many queries the user has typed)
- query: "" | "rea" | "react" = "" (what the search box shows)
- inFlight: set of queries = {} (requests sent, reply not back yet)
- shownFor: "" | "rea" | "react" = "" (which query the list shows results for)

## Actions

- type next
  - Guard: typed < 2
  - Effect: query = the next query, typed + 1, the query joins inFlight

- reply q (per query in flight)
  - Guard: q is in inFlight
  - Effect: q leaves inFlight, shownFor = q

## Properties

### Invariants

- once nothing is loading, the list shows results for what is in the box:
  inFlight is empty implies shownFor === query

## Considerations

- The results themselves are not modeled, only which query they are for.
- Two queries are enough: the bug needs one reply to overtake another.

How it maps to the code:

• query is state.query, and shownFor is which query state.results came from. inFlight is outside the code.
• Each action is one step of the code around its await. type next is onInput up to fetchResults.

Writing it is where most of the thinking happens. The reply q line has to say what the list shows, and “shownFor = q, for any q” is already close to showing the bug.

Step 2: turn the text into Quint (use AI)

The agent writes the Quint. You do not read it: the agent maps it back to the text, and the checks do the rest.

Ask AI to write quint/search.qnt from quint/search.md. One var per variable, one action per action, guards as conditions, the invariant as a val. Above each part, put the line of the text it comes from as a comment. List anything you had to guess.

You do not need to read Quint. To check the result:

• quint typecheck quint/search.qnt passes.
• Every action and rule in the text has its part in the model, with the text line above it.
• The agent’s guesses are answered in the text, not in the model. Then regenerate.

The checker then checks the model (Step 3), and the replay checks that the real code does what the model says (Step 5).

The generated model, and how to read it

A Quint model has variables (the state) and actions (the steps that change it). Each action has a condition for when it can happen, and says what the variables become. x' means “the value of x after this step”.

quint/search.qnt

module search {
  // The user types "rea", then "react".
  pure val QUERIES = ["rea", "react"]

  var typed: int          // how many queries the user has typed
  var query: str          // what the search box shows
  var inFlight: Set[str]  // requests sent, reply not back yet
  var shownFor: str       // which query the list shows results for

  action init = all {
    typed' = 0,
    query' = "",
    inFlight' = Set(),
    shownFor' = "",
  }

  action typeNext = all {
    typed < QUERIES.length(),
    typed' = typed + 1,
    query' = QUERIES[typed],
    inFlight' = inFlight.union(Set(QUERIES[typed])),
    shownFor' = shownFor,
  }

  action reply(q: str): bool = all {
    inFlight.contains(q),
    inFlight' = inFlight.exclude(Set(q)),
    shownFor' = q,
    typed' = typed,
    query' = query,
  }

  action step = any {
    typeNext,
    nondet q = oneOf(inFlight)
    reply(q),
  }

  // Once nothing is loading, the list shows results for what is in the box.
  val listMatchesBox = inFlight == Set() implies shownFor == query
}

How to read it:

• typeNext is the user typing the next query. It sends a request, so the query goes into inFlight.
• reply(q) is the reply for q coming back, in any order. It updates the list, just like state.results = results in the TS code.
• step is what can happen next: the user types, or any request in flight replies. nondet q = oneOf(inFlight) means “any of them”. The checker tries each choice.
• listMatchesBox is the rule, checked in every state.

Step 3: let Quint find the bad order

quint run finds the late reply in milliseconds; quint verify confirms it over all 8 states.

quint run makes random runs and stops at the first state that breaks the rule:

The same trace as a timeline:

quint run is random, so a clean run would not prove much. quint verify checks every reachable state:

Two queries give only 8 states. That is enough to show this bug. Most ordering bugs need only two or three events to show up.

Step 4: fix the model

Show a reply only if it answers what is in the box now. The rule holds in every state.

A reply should only replace the list if it is for the latest request. Change the text first:

Before the fix Diff With the fix

# Search box - spec
The user types "rea", then "react". Each query sends a request, and the replies come
back in any order. The checkable version is search.qnt, next to this file.
## Constants
- queries = "rea", "react" (typed in this order)
## Variables
- typed: 0..2 = 0 (how many queries the user has typed)
- query: "" | "rea" | "react" = "" (what the search box shows)
- inFlight: set of queries = {} (requests sent, reply not back yet)
- shownFor: "" | "rea" | "react" = "" (which query the list shows results for)
## Actions
- type next
  - Guard: typed < 2
  - Effect: query = the next query, typed + 1, the query joins inFlight
- reply q (per query in flight)
  - Guard: q is in inFlight
  - Effect: q leaves inFlight, shownFor = q
  - Effect: q leaves inFlight, shownFor = q only if q === query (a reply for an older query is dropped)
## Properties
### Invariants
- once nothing is loading, the list shows results for what is in the box:
  inFlight is empty implies shownFor === query
## Considerations
- The results themselves are not modeled, only which query they are for.
- Two queries are enough: the bug needs one reply to overtake another.

The agent updates the model to match.

The model change: quint/search.qnt (1 line)

Before the fix Diff With the fix

module search {
  // The user types "rea", then "react".
  pure val QUERIES = ["rea", "react"]
  var typed: int          // how many queries the user has typed
  var query: str          // what the search box shows
  var inFlight: Set[str]  // requests sent, reply not back yet
  var shownFor: str       // which query the list shows results for
  action init = all {
    typed' = 0,
    query' = "",
    inFlight' = Set(),
    shownFor' = "",
  }
  action typeNext = all {
    typed < QUERIES.length(),
    typed' = typed + 1,
    query' = QUERIES[typed],
    inFlight' = inFlight.union(Set(QUERIES[typed])),
    shownFor' = shownFor,
  }
  action reply(q: str): bool = all {
    inFlight.contains(q),
    inFlight' = inFlight.exclude(Set(q)),
    shownFor' = q,
    // A reply is shown only if it answers what is in the box now.
    shownFor' = if (q == query) q else shownFor,
    typed' = typed,
    query' = query,
  }
  action step = any {
    typeNext,
    nondet q = oneOf(inFlight)
    reply(q),
  }
  // Once nothing is loading, the list shows results for what is in the box.
  val listMatchesBox = inFlight == Set() implies shownFor == query
}

No state breaks the rule. The matching TS change keeps a request counter and drops replies that are not the latest:

Before the fix Diff With the fix

export function createSearch(fetchResults: (query: string) => Promise<string[]>) {
  const state = { query: '', results: [] as string[] };
  let latest = 0;
  async function onInput(query: string): Promise<void> {
    const id = ++latest;
    state.query = query;
    const results = await fetchResults(query);
    if (id === latest) state.results = results;
  }
  return { state, onInput };
}

Cancelling the old request with an AbortController works too; the model is the same.

Step 5: replay Quint’s traces against the real TS code (use AI)

Quint writes its runs as JSON traces; vitest replays each one against the real search code.

The model is fixed. Nothing yet says the TS code behaves like the model. To connect them, Quint writes its runs as JSON traces, and a vitest file plays each trace against the real createSearch, step by step, checking the state after every step.

Write the traces:

quint run quint/search.qnt --invariant listMatchesBox --mbt \
  --seed 1 --max-samples 1000 --max-steps 10 \
  --n-traces 50 --out-itf 'quint/traces/run_{seq}.itf.json'

--seed makes the runs repeatable, so a trace that fails in CI fails the same way on your laptop.

The replay test gives the search a fake fetchResults. Each request waits until the trace says its reply comes back, which is how the test controls the order of the replies:

The replay test: src/search.quint.test.ts (55 lines)

src/search.quint.test.ts

import { readdirSync, readFileSync } from 'node:fs';
import { expect, test } from 'vitest';
import { createSearch } from './search';

interface ItfState {
  'mbt::actionTaken': string;
  'mbt::nondetPicks': { q?: { tag: 'Some' | 'None'; value?: string } };
  query: string;
  inFlight: { '#set': string[] };
  shownFor: string;
}

const dir = new URL('../quint/traces/', import.meta.url);
const files = readdirSync(dir).filter((f) => f.endsWith('.itf.json'));

function world() {
  const replies = new Map<string, () => void>();
  const search = createSearch(
    (query) =>
      new Promise<string[]>((resolve) => {
        replies.set(query, () => resolve([`results for ${query}`]));
      }),
  );
  const shownFor = () => search.state.results[0]?.replace('results for ', '') ?? '';
  return { search, replies, shownFor };
}

const settle = () => new Promise((resolve) => setTimeout(resolve, 0));

test.each(files)('%s: the search follows the model and the list matches the box', async (file) => {
  const states: ItfState[] = JSON.parse(readFileSync(new URL(file, dir), 'utf8')).states;
  const { search, replies, shownFor } = world();

  for (const state of states.slice(1)) {
    const action = state['mbt::actionTaken'];
    const q = state['mbt::nondetPicks'].q?.value ?? '';

    if (action === 'typeNext') {
      search.onInput(state.query);
    } else if (action === 'reply') {
      // Let this query's request finish, so onInput goes on.
      replies.get(q)?.();
      replies.delete(q);
    }
    await settle();

    expect({ action, q, query: search.state.query, shownFor: shownFor() }).toEqual({
      action,
      q,
      query: state.query,
      shownFor: state.shownFor,
    });
    if (state.inFlight['#set'].length === 0) expect(shownFor()).toBe(search.state.query);
  }
});

First, save the counterexample from Step 3 as a trace (--out-itf quint/traces/bug.itf.json with the seed Quint printed) and replay it against the original code:

The real code followed the model at every step, and then left the results for “rea” under a box that says “react”. The Quint counterexample is now a failing vitest on your real code, with the exact order that breaks it. That is a bug report nobody has to reproduce by hand.

After the fix, replace the traces with 50 runs of the fixed model and replay them against the fixed code:

To check the replay is not passing by accident: the old bug trace against the fixed code fails on the last reply step. The model expected the list to show “rea”, the fixed code had dropped that stale reply and still showed “react”. The replay notices when the code and the model differ, not just when the rule breaks.

Project layout and CI

Traces are regenerated on every test run with a fixed seed, and never committed.

One repo. The model sits in its own folder. The traces are built from it on every test run and never committed:

./
├── .github/workflows/ci.yml
├── quint/
│   ├── search.md                the model in plain text: written with the agent, reviewed by people
│   ├── search.qnt               the same model in Quint, generated from the text
│   └── traces/                  generated before every test run, git-ignored
├── src/
│   ├── search.ts                the real search code
│   ├── search.test.ts           normal unit tests
│   └── search.quint.test.ts     replays quint/traces/ against search.ts
├── .gitignore                   node_modules, quint/traces/, _apalache-out/
├── package.json
└── tsconfig.json

Quint goes in devDependencies:

npm i -D @informalsystems/quint

Scripts in package.json:

"scripts": {
  "quint:check": "quint typecheck quint/search.qnt && quint verify quint/search.qnt --invariant listMatchesBox --backend tlc",
  "quint:traces": "rm -rf quint/traces && mkdir -p quint/traces && quint run quint/search.qnt --invariant listMatchesBox --mbt --seed 1 --max-samples 1000 --max-steps 10 --n-traces 50 --out-itf 'quint/traces/run_{seq}.itf.json' > /dev/null",
  "pretest": "npm run quint:traces",
  "typecheck": "tsc",
  "test": "vitest run"
}

pretest runs before npm test, so the replay always uses traces from the current model.

The CI workflow has two jobs. Only the quint job needs Java:

The CI workflow: .github/workflows/ci.yml (45 lines)

.github/workflows/ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  quint:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: actions/setup-java@v6
        with:
          distribution: temurin
          java-version: 21
      - uses: actions/setup-node@v7
        with:
          node-version: 24
          cache: npm
      - uses: actions/cache@v6
        with:
          path: ~/.quint
          key: quint-${{ hashFiles('package-lock.json') }}
      - run: npm ci
      - name: Check every state of the model
        run: npm run quint:check

  ts:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: actions/setup-node@v7
        with:
          node-version: 24
          cache: npm
      - uses: actions/cache@v6
        with:
          path: ~/.quint
          key: quint-${{ hashFiles('package-lock.json') }}
      - run: npm ci
      - run: npm run typecheck
      - name: Replay model traces against the real code
        run: npm test

What fails when:

Change	Where CI fails
A model change breaks the rule	quint job, quint verify: the counterexample is in the log. The ts job fails too, since quint run stops at the violation
The search code changes and no longer follows the model	ts job, search.quint.test.ts: the first step where the screen and the model differ
The model changes, the code does not	ts job: the new traces no longer match the old code
The fake fetchResults in the replay no longer matches the real signature	ts job, tsc

Making changes

Change the model first and check it, then change the code until the replay passes.

Changing the flow (for example, clearing the list when the box is emptied):

1. Change the text model first: a new action, the variables it touches, and a rule if there is a new “must never happen”.
2. Ask the agent to update search.qnt from it, and to list what it changed in the words of the text.
3. Run npm run quint:check with the two queries, then add a third once it passes.
4. Change the code. Map the new action to a step in search.quint.test.ts (which call to make, which reply to release).
5. Run npm test until the replay passes. Commit the text, the model, the code and the replay test together.

Adding a rule: add a val to the model and add it to --invariant in both scripts. If the real code can break it without breaking the model, the replay test needs the same check (like the list-matches-box check there).

When CI finds a counterexample: copy the trace from the quint verify log or rerun quint run with the seed it prints. Write it to a file with --out-itf to replay it locally against the code. Fix the model or the code, and the next run checks every state again.

Reviewing a pull request: read the text model diff. A new await in the code with no new step in the text means the model no longer splits the code where it can interleave. That is the one mistake the replay cannot catch, because the replay follows the model’s steps.

Strengths

• Every order of steps is checked. Quint tries them all in the model, in under a second at this size.
• A short, readable failing trace. You get the shortest order that breaks the model, not a flaky test that fails once a week.
• Fixes checked before code. You can check a fix in the model before you write it in TS.
• Traces become tests. Each trace turns into an ordinary vitest case for the real code.

Limitations

• No proof about the TS code. quint verify checks the model. The replay checks the code only on the traces you replay, here 50 random runs.
• The model takes effort. You choose where the steps split. If you merge steps that the real code keeps apart, the model hides the bug.
• Only what the model has. This model has no failure step, so Quint says nothing about a request that rejects.
• Small numbers only. Checking every state works for a few events and a few actors. That usually finds the bug, but it is not a load test.

How to start in your own project

1. Pick one flow where order matters: a search box, a webhook, a job queue, a retry loop, a lock.
2. Write a text model next to the code. List the variables, including the ones outside your code: requests in flight, retries, what each actor has seen.
3. Make one action per step between two awaits in the real code, and write the rule as “this must never happen”.
4. Let an agent turn the text into Quint, with each part tagged by the line of the text it comes from.
5. Run quint run first (fast), then quint verify (every state), with 2 or 3 actors.
6. Export traces with --mbt --out-itf and a fixed --seed, and replay them against the real code with controlled fakes.

Related

• Quint getting started
• Summary of the Quint language
• Model-based testing with Quint
• Quint on GitHub
• TLA+ for TypeScript developers, the method underneath, used directly.