Roadmap

Each milestone is one reviewable change set: small, self-contained, with its own tests, and useful on its own. Nothing starts before the previous milestone's acceptance criteria are met.

---

M0 — Skeleton (done)

Project layout, deps.edn, docs, ADRs, ITF fixtures recorded from Quint 0.32.0, metadata mechanics verified against Clojure 1.12.5. No library code.

---

M1 — itf: decode (done)

Pure ITF JSON -> EDN.

• Decode #bigint, #map, #set, #tup, records and sum types ({tag, value}). #unserializable is deferred: Quint's writer never emits it, only its reader accepts it, so no recording exists to test against. M7b was expected to settle this and did — Apalache's counterexamples carry none either, so it is deferred indefinitely rather than to a milestone.
• Unwrap Some/None only inside mbt::nondetPicks, where Quint's own runtime puts it regardless of what the spec declares; None drops the key. Those tags in an ordinary state variable are a type the spec declared itself and decode like any other variant.
• Decode the bignumber.js form Quint leaks for integers >= 10^15 ({s, e, c}); the reconstruction rule is in notes/itf-format.md.
• Normalize variable names: bankTest::bank::balances -> :balances; error on collision; :key-fn option to override. Names are not kebab-cased — Quint is camelCase and round-tripping matters more than Clojure aesthetics.
• Split mbt::actionTaken / mbt::nondetPicks out of the state into :action / :picks.

Done when: every dev/fixtures/*.itf.json decodes to the expected EDN — collide_0 excepted, which is recorded precisely to fail without a :key-fn — the two bigint fixtures decode identically, and #meta noise (timestamp, description) is ignored.

---

M2 — replay + report: the loop (done)

No subprocess, no file I/O, no metadata — this milestone consumes a resolved driver map that the tests build by hand. The only effects are the ones the driver's own functions perform.

• (replay/run-trace driver trace) -> result data as specified in architecture.md §6, including the coverage report.
• The loop: init, read state, compare to state 0; then for each following state, call the handler with its picks, read state, compare; halt in a finally. Stop at the first mismatch.
• State is read through the driver's readers on every step. Handler return values are discarded.
• Unknown action, throwing handler, failing reader: structured results or typed ex-info.
• report/failure-str renders step index, action, picks, handler var, reader vars, and a readable diff.

Done when: a hand-written driver over an atom passes against the committed bank fixture; a deliberately broken one fails at exactly the expected step with a diff a human can act on; an init that forgets to reset fails at step 0 of the second trace.

---

M3 — registry: the annotations (done)

The reflective layer, and the reason the project has the shape it has. It turns :quint/* metadata into the driver map M2 already consumes.

• require each namespace in :scan, read ns-interns, collect annotations from the var and, for IReference values, from the object too.
• Read the qualifier from the driver's :key-ns (a symbol, default quint), in one place. All keys move together; there is no per-key override. M3 shipped five of them; :quint/driver joined the set later, in decisions/0009-driver-scope.md.
• :quint/action -> handler, picks bound positionally from :arglists; :quint/args overrides; multi-arity without it is :ambiguous-arity.
• :quint/state on a function var (called with no arguments) and on an IDeref var (dereferenced), then :path via get-in; :* merges a whole map of spec variables.
• :quint/init / :quint/halt -> the per-trace lifecycle.
• Merge the driver map over the scan result; the map wins.
• Validate loudly, at construction: :empty-scan (naming the ^{...} (defn ...) trap), :duplicate-action, :duplicate-state, :ambiguous-arity. :no-init needs the trace and so belongs to replay; :missing-state needs the spec's variable list, which the driver never sees, and is not built — see architecture.md §5.
• Rebuild on every call. No global registry atom, ever.

Done when: a fixture namespace with every annotation form resolves to the exact driver map M2 was tested against; each validation error has a test; the metadata trap produces a message that names it.

---

M4 — quint: talk to the CLI (done)

• Build the command for run (--mbt --seed --n-traces --max-samples --max-steps --out-itf --verbosity 0), run it in a temp dir with clojure.java.process, and read back the files.
• Note: --max-samples is attempts, --n-traces is traces written. Expose both; do not silently equate them the way quint-connect does.
• Random seed generation, and print the reproduce line on failure.
• Check quint --version once, warn on drift from the tested version.

Done when: traces are generated from dev/fixtures/bank.qnt, temp dirs are cleaned, and a missing binary / broken spec / zero traces each produce a clear typed error carrying Quint's own stderr verbatim.

---

M5 — core + test: usable (done)

• q/driver, q/defdriver, q/check, q/replay-file, plus the clojure.test bridge that turns a result map into one assertion with a good message.
• A real toy bank implementation in dev/, annotated, with a real deftest.

Done when: bb test runs a genuine model-based test end to end; injecting a bug into the toy implementation produces a failure naming the action, the handler var, the step, the diff, and the seed to reproduce.

---

M6 — Failure artifacts (done)

Turn a failure into a permanent regression test.

• qt/check writes the failing trace to test-resources/quint-connect/failures/ — Quint's bytes verbatim, under a deterministic <spec>-seed<seed>-trace<index>.itf.json. qt/save-failure! is the same step as a function; :save-failure turns it off or moves it.
• The drop zone is gitignored and the archive is not: promotion into test-resources/quint-connect/ is a mv a human performs, so a failing run never dirties the repository.
• q/replay-file reads it back with no Quint installed; qt/replay-file asserts on the result.
• The workflow is documented in getting-started.md §6 and architecture.md §7.

Done when: the documented loop works from a cold checkout without Quint.

---

M7a — Scripted runs (done)

M7 was split in two: this half needs no new tool, and the other half brings a second model checker, minute-long runs and its own error taxonomy. :action-path is a prerequisite for both, since neither quint test nor quint verify emits mbt:: variables.

• :action-path / :nondet-path: read the action name and the picks from ordinary spec variables. Each path's root variable is split out of the compared state — the spec's bookkeeping is not state the implementation has to supply. This is also what Choreo-style specs need.
• q/check-run and qt/check-run — the trace of a named Quint run, via quint test --match.
• dev/fixtures/tracked.qnt: the bank again, recording its own action, so the unchanged dev/bank/core.clj replays it.

Done when: a spec that tracks its own action drives the driver, from a quint test trace with no mbt:: variables in it.

---

M7b — verify (done)

• q/verify — run Apalache through quint verify, treat "invariant holds" as a pass, and replay the counterexample against the implementation when it does not.
• The behaviour this rests on is recorded in notes/itf-format.md §quint verify and reproducible with dev/probes/verify_probe.sh.
• The open question is answered, and not the way it was guessed. --apalache-config does not move _apalache-out/, and the name is Apalache's to choose, not ours. What it does follow is the working directory, so running verify in a scratch directory contains it and deletes it — at the cost of the untested "sibling modules resolve" rationale for running in the spec's own directory, which is the one thing left to decide.
• All four failure modes exit 1. The discriminator is whether a trace was written, not the exit code and not the wording.
• An invariant that holds writes no trace, so zero traces is the pass and verify! cannot reuse :no-traces.
• Needs its own test tag and bb task, so bb test:all stays fast.
• #unserializable stays deferred, now with a recording to back that up: the counterexample contains none, and the dialect decodes through itf unchanged. M7b does not grow that namespace.

Done when: a spec with a deliberate invariant violation produces a counterexample that replays against the implementation. — Done. tracked.qnt gained underFifty, violated by a single deposit, and tracked_verify_underFifty.itf.json is the recorded counterexample, replayed by bb test with no Apalache anywhere. bb test:verify runs the real thing.

---

M8 — Ergonomics, only after the above is boring

Candidates, in rough priority order. Each needs its own justification when its turn comes; none is committed to now.

• cli — generate and cache traces into test-resources/, so CI can run without Quint. It brings its own deps.edn alias; there is deliberately no alias pointing at a namespace that does not exist yet.

• :setup / :teardown in the driver map, run once per check. Only if something real needs it: clojure.test/use-fixtures and a let around the call already cover the container-per-run case without new machinery.

• :missing-state at the first comparison — name the spec variables that no reader supplies, instead of diffing them against nothing.

• Richer annotations, only where a real spec demanded them: :quint/action with a set of names, per-var :quint/compare, :quint/ignore.

• Variant handling configurable per driver, or per variable: a :variants option on the decoder, additive to the existing :key-fn. Not built now — leaving variants wrapped is the reversible choice, and a state reader or :compare already covers it without new machinery.

• Kaocha plugin: seed reporting, per-trace progress, --focus on a trace file. Roughly 100 lines against kaocha.hierarchy. Optional, separate artifact with its own deps.edn. Later — after the linter, which every user benefits from rather than only Kaocha users.

• clj-kondo hooks so annotated vars and unknown :quint/* keys are linted. Half done. The defdriver half shipped: the jar now carries a clj-kondo export, so a consumer's linter stops reporting every driver name as an unresolved symbol without them configuring anything. What is left is the annotations: a misspelled :quint/actoin, a :quint/args shape that cannot compose, an annotation stranded under the wrong :key-ns. The last of those is the gap 0007 accepts at runtime and a linter is the one place it could be closed without a namespace-similarity heuristic.

  That half is not free, which is why it did not ship with the other. Metadata on a defn is not a call, so the only hook that sees it is one on clojure.core/defn — and an exported config carrying that would run on every defn in a consumer's project to serve the handful that are annotated. If it is built, it belongs behind a config a user opts into, not in the export.

• Shrinking. Probably never: the first diverging step is already the minimal information, and dropping steps from a state machine trace produces traces the spec never generated.

• witnesses / --invariants support for targeted trace generation.

• Choreo support, end to end. A later release, and the biggest single thing missing. Choreo is where the Quint ecosystem is pointed. Recorded on 2026-08-26 by running Choreo's own two_phase_commit.qnt under --mbt, replacing what this entry used to infer:

  vars: ["two_phase_commit::choreo::s", "mbt::actionTaken", "mbt::nondetPicks"]
  
  index 1  actionTaken: "step"
           picks: {v: Some("p3"),
                   transition: Some({post_state: {process_id: "p3",
                                                  role: Participant,
                                                  stage: Aborted},
                                     effects: Set()})}
  

  Three things follow, and only the first was guessed right before.

  1. mbt::actionTaken is "step" on every step. One name, so nothing dispatches on it. (The earlier guess said process_transitions; it is the outer action, not the inner one.)
  2. The picks are richer than expected: they carry the acting process and the whole chosen transition. But a transition is {post_state, effects} — an outcome, with no name anywhere in it.
  3. All state is one variable, s, holding {events, extensions, messages, system}, with system a map of process to local state.

  So a Choreo spec can drive an implementation, and not the way this entry assumed. Since every step is "step", one driver-map entry catches all of them and receives both picks:

  :actions {"step" (fn [{:keys [v transition]}] ...)}   ; node, and its post-state
  

  and the mapping from an outcome back to the operation that produces it is adaptation in the test namespace, which is where this design already says adaptation belongs. State comes back through one reader supplying :s.

  What this does not reach is dispatch by transition name, because Choreo records none. The instrumentation Quint's docs mention would put a name in the local state — and :action-path could not read it there anyway, because it is a static get-in path and the node that acted is a pick, different on every step. Letting :action-path and :nondet-path take a function of the decoded state and picks, not only a vector, is the change that would close that. Noted, not committed to.

  What is genuinely left is the example: a Clojure two-phase commit and the adapter above, green. It needs Choreo's four .qnt files vendored — 30 KB, Apache-2.0, so attribution rather than a licence problem — and vendoring is a dependency decision that wants its own ADR under the rule in CLAUDE.md.