@firfi/quint-connect

Model-based testing framework connecting Quint specifications to TypeScript implementations. The TypeScript equivalent of quint-connect (Rust).

Spawns quint run --mbt, parses ITF traces, replays them through a user-implemented driver, and optionally compares spec state against implementation state after every step.

Install

# Simple API (default):
pnpm add @firfi/quint-connect

# If using Zod ITF schemas (ITFBigInt, ITFSet, ITFMap) — requires Zod 4+:
pnpm add zod

# For Effect API:
pnpm add @firfi/quint-connect effect

# For Effect vitest helper (quintIt):
pnpm add -D @effect/vitest

Requirements: Node.js 21+ (for import.meta.dirname), ESM ("type": "module" in package.json), Quint CLI (npx @informalsystems/quint runs without global install).

Usage

Given a Quint spec counter.qnt:

module counter {
  var count: int
  action init = { count' = 0 }
  action Increment = {
    nondet amount = Set(1, 2, 3).oneOf()
    count' = count + amount
  }
  action step = any {
    Increment,
  }
}

Write a driver and run:

import { defineDriver, run, stateCheck } from "@firfi/quint-connect"
import { ITFBigInt } from "@firfi/quint-connect/zod"
import { z } from "zod"

const CounterState = z.object({ count: z.bigint() })

const result = await run({
  spec: "./counter.qnt",
  nTraces: 10,
  maxSteps: 20,
  seed: "1",
  driver: defineDriver(
    { init: {}, Increment: { amount: ITFBigInt } },
    () => {
      let count = 0n
      return {
        init: () => {},
        Increment: ({ amount }) => {       // amount: bigint — inferred from schema
          count += amount
        },
        getState: () => ({ count }),
      }
    }
  ),
  stateCheck: stateCheck(
    (raw) => CounterState.parse(raw),
    (spec, impl) => spec.count === impl.count,
  ),
})

console.log(result.tracesReplayed, result.seed)

Per-field pick schemas use Standard Schema — Zod, Valibot, ArkType, or any compatible library. ITF values ({"#bigint":"5"}) are automatically transformed to native types (5n) before schema validation.

State checking is optional — omit stateCheck for smoke-testing (verifying the driver doesn't crash on spec actions).

ITF Type Mappings

All Quint values are automatically transformed from ITF encoding to native JS types before schema validation:

Quint type	JS type	Schema
int	bigint	ITFBigInt / z.bigint()
str	string	z.string()
bool	boolean	z.boolean()
Set(T)	Set<T>	ITFSet(inner) / z.set(inner)
T -> U (Map)	Map<K,V>	ITFMap(k, v) / z.map(k, v)
(T1, T2) (Tuple)	[T1, T2]	z.tuple([...])
{ field: T } (Record)	{ field: T }	z.object({ field: ... })

Note: All Quint int values become bigint, not number. Use 0n literals and z.bigint() / ITFBigInt.

See examples/counter/counter.test.ts for a complete runnable vitest example.

Effect API

For full control (custom error channels, services, resource management), import from @firfi/quint-connect/effect:

import { defineDriver, quintRun, stateCheck, ITFBigInt } from "@firfi/quint-connect/effect"
import { Effect, Schema } from "effect"

const CounterState = Schema.Struct({ count: ITFBigInt })

const result = await Effect.runPromise(
  quintRun({
    spec: "./counter.qnt",
    nTraces: 10,
    maxSteps: 20,
    seed: "1",
    driverFactory: defineDriver(
      { init: {}, Increment: { amount: ITFBigInt } },
      () => {
        let count = 0n
        return {
          init: () => Effect.void,
          Increment: ({ amount }) =>         // bigint — inferred from schema
            Effect.sync(() => {
              count += amount
            }),
          getState: () => Effect.succeed({ count }),
        }
      }
    ),
    stateCheck: stateCheck(
      (raw) => Schema.decodeUnknown(CounterState)(raw).pipe(Effect.orDie),
      (spec, impl) => spec.count === impl.count,
    ),
  })
)

console.log(result.tracesReplayed, result.seed)

No Effect.scoped or Effect.provide needed — resource management and Node.js services are handled internally.

See examples/counter/counter-effect.test.ts for a complete runnable vitest example.

Vitest Helpers

Simple API helper (no Effect dependency needed):

import { quintTest } from "@firfi/quint-connect/vitest-simple"
import { test } from "vitest"

quintTest(test, "my test", {
  spec: "./myspec.qnt",
  driver: myDriver,
})

Effect API helper (requires @effect/vitest):

import { quintIt } from "@firfi/quint-connect/vitest"
import { it } from "@effect/vitest"

quintIt(it.effect, "my test", {
  spec: "./myspec.qnt",
  driverFactory: myDriver,
})

The first argument is the test function from your own vitest/@effect/vitest instance — this avoids vitest instance collisions when the library and your project use different vitest versions. Both accept an optional fourth argument for timeout (default: 30s).

API

Simple API (@firfi/quint-connect)

• defineDriver(schema, factory) — define a typed driver with per-field Standard Schema picks. schema maps action names to { fieldName: StandardSchema }. factory returns handlers (with inferred pick types) + optional getState/config. Compile error if a handler is missing. Actions with no nondet picks use an empty schema: { Toggle: {} }.
• stateCheck(deserialize, compare) — helper that infers the state type from deserialize and contextually types compare's parameters. Needed because TypeScript cannot infer generic type parameters across sibling callbacks in an object literal.
• run(opts) — generate traces and replay them through a driver. Returns Promise<{ tracesReplayed, seed }>.

Effect API (@firfi/quint-connect/effect)

• defineDriver(schema, factory) — define a driver with per-field Effect Schema picks. Same shape as simple API but handlers return Effect.
• stateCheck(deserialize, compare) — same as simple API but deserialize returns Effect<S>.
• quintRun(opts) — generate traces via quint run --mbt and replay them through a driver. Returns Effect<{ tracesReplayed, seed }>.
• generateTraces(opts) — just spawn quint and parse ITF traces without replaying.
• ItfOption(schema) — Effect Schema that decodes Quint's Option variant to A | undefined.
• ITFBigInt, ITFSet(item), ITFMap(key, value) — ITF type schemas.

RunOptions

Shared by run, quintRun, and generateTraces:

Field	Type	Default	Description
spec	string	required	Path to the .qnt spec file
seed	string	random	RNG seed for reproducible runs. Must be a big integer: decimal ("42") or hex ("0x138ff8c9"). Also reads QUINT_SEED env var as fallback. When omitted, a random hex seed is generated and returned in result.seed for reproducibility.
nTraces	number	10	Number of traces to generate
maxSteps	number	quint default	Maximum steps per trace
maxSamples	number	quint default	Maximum samples before giving up on finding a valid step
init	string	quint default	Name of the init action
step	string	quint default	Name of the step action
main	string	quint default	Name of the main module. Required when the .qnt file contains multiple modules.
backend	"typescript" | "rust"	"typescript"	Simulation backend. TypeScript works out of the box; "rust" requires the Rust evaluator.
invariants	string[]	—	Invariant names to check during simulation
witnesses	string[]	—	Witness names to report
verbose	boolean	false	Sets QUINT_VERBOSE=true. Quint logs detailed simulation output to stderr.
traceDir	string	temp dir	Directory to write ITF trace files. Files are kept after run. Useful for debugging — inspect generated traces when a test fails.

run additionally accepts:

Field	Type	Description
driver	() => SimpleDriver<State>	Creates a fresh action-map driver per trace. Use defineDriver to create.
stateCheck	stateCheck(deserialize, compare)	Optional. Compare spec vs impl state after each step. Use stateCheck() helper for type inference.

quintRun additionally accepts:

Field	Type	Description
driverFactory	{ create: () => Effect<Driver<S, E, R>> }	Creates a fresh action-map driver per trace. Use defineDriver to create.
stateCheck	stateCheck(deserialize, compare)	Optional. Compare spec vs impl state after each step. Use stateCheck() helper for type inference.

Config

Drivers can optionally return a Config from config():

Field	Type	Default	Description
statePath	string[]	[]	Path to extract state subtree for deserializeState/compareState
nondetPath	string[]	[]	Nested path to a sum-type action encoding (Choreo-style specs)

statePath scopes what deserializeState and compareState receive. If your Quint module wraps all state in a single record variable:

var routingState: { count: int }

Set statePath: ["routingState"] so that deserializeState receives { count: ... } directly instead of { routingState: { count: ... }, "mbt::actionTaken": ..., ... }.

When using statePath, both deserializeState and getState should work with the scoped state shape (e.g. { count }, not { routingState: { count } }).

Init action handling

Step 0 (the init state) is processed like any other action, matching the Rust quint-connect behavior. The mbt::actionTaken field determines the action name.

With the Rust backend (backend: "rust"), init has a proper action name (e.g. "Init") — define it in your action map if you want it dispatched. If it is not mapped, replay fails with TraceReplayError; if it is mapped, state comparison runs at step 0 too.

With the TypeScript backend (default), some traces report an empty mbt::actionTaken at step 0; only that empty placeholder is skipped. If the trace reports a non-empty action such as "init", define that action in your map or replay fails with TraceReplayError.

Additional Exports

@firfi/quint-connect/effect also exports: ITFList, ITFTuple, ITFVariant, ITFUnserializable, ItfTrace, MbtMeta, UntypedTraceSchema, generateTraces, defaultConfig.

@firfi/quint-connect also exports: transformITFValue, defaultConfig.

@firfi/quint-connect/zod also exports: TraceCodec.

Error Handling

The library exports typed error classes for programmatic error handling:

Error	Trigger
TraceReplayError	Unknown action, handler failure, decode failure
StateMismatchError	compareState returns false
QuintError	quint run exits non-zero (includes stderr output)
QuintNotFoundError	quint CLI not found
NoTracesError	quint run produced no traces

Simple API — use instanceof:

import { run, StateMismatchError, TraceReplayError } from "@firfi/quint-connect"

try {
  await run(opts)
} catch (e) {
  if (e instanceof StateMismatchError) {
    console.log(e.expected, e.actual, e.traceIndex, e.stepIndex)
  }
}

Effect API — use catchTag:

quintRun(opts).pipe(
  Effect.catchTag("StateMismatchError", (e) =>
    Effect.log(e.expected, e.actual)),
)

StateMismatchError has traceIndex, stepIndex, expected, actual. TraceReplayError has traceIndex, stepIndex, action, cause.

Deterministic specs

For specs with no nondet picks (only one possible execution), use:

{ nTraces: 1, maxSamples: 1, maxSteps: N }

The default nTraces is 10, which would generate 10 identical traces for a deterministic spec.

Backend

The default backend is "typescript" (zero extra deps, works out of the box). Override with backend: "rust" for the more mature Rust evaluator (requires separate download).

Known issue: --backend typescript corrupts mbt::actionTaken for specs where the step action is a single body (not any { ... } with named disjuncts). All states will show actionTaken: "init" instead of the actual action name. This is a Quint bug in the TypeScript simulator's Context.shift() — it doesn't reset metadata between steps. Specs using any { ... } are unaffected.

License

Apache-2.0