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

try {
  await run(opts)
} catch (e) {
  if (e instanceof StateMismatchError) {
    console.log("State diverged at trace", e.traceIndex, "step", e.stepIndex)
    console.log("Expected (spec):", e.expected)
    console.log("Actual (impl):", e.actual)
  }
  if (e instanceof TraceReplayError) {
    console.log("Action failed:", e.action, "at step", e.stepIndex)
    console.log("Cause:", e.cause)
  }
}

import { quintRun } from "@firfi/quint-connect/effect"

quintRun(opts).pipe(
  Effect.catchTag("StateMismatchError", (e) =>
    Effect.log("Diverged at", e.traceIndex, e.stepIndex, e.expected, e.actual)),
  Effect.catchTag("TraceReplayError", (e) =>
    Effect.log("Action", e.action, "failed:", e.cause)),
)

Every run/quintRun result includes a seed. Pass it back to get the exact same traces:

// First run — failure reported
const result = await run({
  spec: specPath,
  driver: myDriver,
  nTraces: 10,
})
// result.seed = "0x138ff8c9"

// Reproduce — same traces, same failure
const result2 = await run({
  spec: specPath,
  driver: myDriver,
  nTraces: 10,
  seed: "0x138ff8c9",
})

The seed can also be set via QUINT_SEED environment variable.

Use traceDir to persist trace files for manual inspection:

await run({
  spec: specPath,
  driver: myDriver,
  traceDir: "./debug-traces",
})

Then read the JSON files in ./debug-traces/ to see the raw ITF state at each step. Look for:

• mbt::actionTaken — which action was dispatched
• mbt::nondetPicks — what nondeterministic values were chosen
• State variable keys — verify fully-qualified names

Before writing any driver code, run quint directly to see what it produces:

npx @informalsystems/quint run --mbt \
  --max-samples 1 --max-steps 3 \
  specs/counter.qnt

This shows the exact ITF output: variable names, ITF encoding, action names. Inspect this before guessing at schema shapes.

NoTracesError means quint ran but produced zero trace files. Common causes:

1. Wrong module name — multi-module specs require --main:
   ts

   await run({ spec: specPath, main: "counter_test" })
   

2. Unsatisfiable spec — the init or step action's preconditions are never satisfied. Check the spec logic.
3. Wrong spec path — the file doesn't exist or isn't a valid .qnt file.

Quint CLI must be on PATH. Install it:

pnpm add -D @informalsystems/quint

Or ensure it's available globally. npx @informalsystems/quint works without global install.

Wrong:

const state = { items: new Map() }
return {
  getState: () => state,
}

Correct:

const state = { items: new Map() }
return {
  getState: () => ({ items: new Map(state.items) }),
}

The runner captures state after each step for comparison. Returning a live reference means the captured "expected" snapshot mutates when the next step runs. All comparisons pass vacuously.

Source: maintainer interview

Wrong:

// Test failed, try again:
await run({ spec: specPath, nTraces: 10 })
// Different random traces, different failure — or no failure at all

Correct:

// Use the seed from the failed run's output:
await run({ spec: specPath, nTraces: 10, seed: "0x138ff8c9" })
// Exact same traces, exact same failure

Without a seed, quintRun generates new random traces each time. The original failure may not reproduce. Always capture and reuse the seed.

Source: README.md

Wrong:

stateCheck(deserialize, (spec, impl) => {
  const { internalField: _, ...specRest } = spec
  const { internalField: __, ...implRest } = impl
  return deepEqual(specRest, implRest)
})

Correct:

stateCheck(deserialize, (spec, impl) =>
  spec.count === impl.count && spec.flag === impl.flag
)

When state diverges, the Quint spec is the source of truth. Ignoring fields, sorting maps, or adding exceptions to the comparator masks real implementation bugs. Fix the TS code to match the spec.

Source: maintainer interview

Wrong:

await run({ spec: specPath, nTraces: 1, maxSteps: 50 })

Correct:

await run({ spec: specPath, nTraces: 10, maxSteps: 50 })

A single trace covers one random execution path. Bugs on other paths pass CI and merge. 10 traces with 50 steps covers diverse paths without being excessively slow.

Source: maintainer interview

Wrong:

await run({ spec: "../../specs/counter.qnt" })

Correct:

import * as path from "node:path"
const specPath = path.join(import.meta.dirname, "specs", "counter.qnt")
await run({ spec: specPath })

Relative paths like ../../specs/counter.qnt depend on the working directory. They work locally but break in CI where the test runner may use a different cwd.

Source: examples/counter/counter.test.ts

Wrong:

stateCheck(
  (raw) => Schema.decodeUnknown(MyState)(raw).pipe(Effect.orDie),
  (spec, impl) => spec.count === impl.count,
)

Correct:

stateCheck(
  (raw) => Schema.decodeUnknown(MyState)(raw),
  (spec, impl) => spec.count === impl.count,
)

Effect.orDie converts decode failures to untyped defects. This loses the structured TraceReplayError context (traceIndex, stepIndex, action) that helps diagnosis. Fine for prototyping; in CI, let errors propagate with full context.

Source: maintainer interview

Patterns that work during prototyping (Effect.orDie, nTraces: 1, partial state comparison) silently mask bugs in production. When optimizing for quick setup, agents omit the robustness that makes MBT testing valuable. Use nTraces: 10+, compare all state fields, and preserve structured error context.

See also: quint-connect-ts-setup/SKILL.md

See also: quint-connect-ts-itf-decoding/SKILL.md -- decode errors often surface as TraceReplayError