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.
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.
itf: decode (done)Pure ITF JSON -> EDN.
#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.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.>= 10^15
({s, e, c}); the reconstruction rule is in
notes/itf-format.md.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.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.
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.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.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.
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.: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.: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.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.
quint: talk to the CLI (done)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.--max-samples is attempts, --n-traces is traces written. Expose
both; do not silently equate them the way quint-connect does.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.
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.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.
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.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.Done when: the documented loop works from a cold checkout without Quint.
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.
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.quint verify and reproducible
with dev/probes/verify_probe.sh.--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.verify! cannot reuse :no-traces.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.
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.
Refusal checks: the other direction. Moved to techdebt.md, status maybe.
TLC counterexamples. Blocked on Quint writing them; upstream/quint-tlc-itf.md is the proposal.
Choreo support left this list: it is M9, below.
Choreo is where the Quint ecosystem is pointed, and it was the biggest single thing missing.
Choreo's own two_phase_commit.qnt, run under --mbt:
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()})}
mbt::actionTaken is "step" on every step. One name, so nothing
dispatches on it.{post_state, effects}, an outcome with no name in it.s, holding {events, extensions, messages, system}, with system a map of process to local state.So a Choreo spec as written can drive an implementation through one driver-map
:actions {"step" ...} entry that maps an outcome back to an operation. That
reaches check and nothing else: quint test and quint verify emit no picks
at all, and coverage can only ever say "step".
CustomEffect(RecordAction(DecidesOnCommit({ node: ... }))), and the effect
processor writes it into s.extensions.actionTaken. Quint's own blog
describes Choreo testing the same way. A variant's tag is the action name
and its record is the picks.s, it is in every trace: quint run --mbt and quint test alike. Recorded both; commitTest comes out of
quint test naming each transition with no mbt:: anywhere.Init carries the empty tuple, {"tag": "Init", "value": {"#tup": []}},
which decodes to [] — not a record of picks.AbortsAsInstructed for participants that
had already aborted. (Fixed after review: the spec now filters them itself —
see below.)quint verify fails on every Choreo spec, instrumented or not, on Quint
0.32.0 and on 0.33.0 (released 2026-09-28): internal error in type checking: A typed declaration two_phase_commit::choreo::s was transformed to an untyped expression. Choreo's own Tendermint fails the same way. The
message is Apalache's — its type watchdog, TypeWatchdogTransformationListener
in apalache.jar, rejecting what Quint hands it — under Apalache 0.56.1 and
0.62.1, while quint compile --target=tlaplus of the same spec succeeds.
Whose bug it is was not established. What it means here is that there is no
Choreo counterexample to record. q/verify surfaces the failure as
:quint-failed with that stderr verbatim, which is the right behaviour and
all this library can do. Reproducible with dev/probes/choreo_probe.sh.
After review: reduced to thirteen lines — a state variable whose type has
a type parameter fixed only by instantiation — present from Quint 0.28.0 on;
and --backend=tlc checks Choreo specs, without writing a trace.choreo.qnt beside its spells/.The current library already replays the instrumented convention, except for two things, and one of them is silent.
:action-path [:s :extensions :actionTaken :tag] does read the action. But a
path's root variable leaves the compared state, and in a Choreo spec the root
is s — which is all of the state. What is left to compare is nothing, and
every step passes: through driver-map handlers that do nothing, the
recorded commitTest replays green. That is the failure mode this design is
most exposed to, reached by writing the paths the obvious way.
Library changes, in itf only, with core passing one more key through:
:state-path, a vector in the driver map. The compared state is the
record found there, and its fields stand in for spec variables from then on:
{:state-path [:s]} compares :system, :messages, :events and
:extensions, and a reader annotated {:quint/state :system} supplies one of
them. It is applied first; :action-path and :nondet-path are read inside
it, and each root still leaves the compared state, so
[:extensions :actionTaken :tag] removes exactly the bookkeeping.
:bad-decode-path when it is not a vector, finds nothing, or finds something
that is not a record.:nondet-path accepts [], Quint's
encoding of a variant without an argument, as {}. Anything else that is
not a record is still refused.:action-path and :nondet-path leaves nothing to compare, decoding
fails with :bad-decode-path, naming :state-path as the likely fix.No new public function. itf/itf->trace keeps its signature and gains an
option; core/driver passes :state-path through with the others.
Around it:
choreo.qnt and spells/basicSpells.qnt at commit
000cf4e, with Choreo's Apache-2.0 licence beside them. A dependency
decision, so 0012; the decoding choices
are 0013.dev/fixtures/choreo/: Choreo's two_phase_commit.qnt
(import paths adjusted, nothing else) recorded under --mbt, and
two_phase_commit_tracked.qnt — the same, instrumented — recorded under
--mbt and under quint test.dev/tpc/core.clj, a small annotated two-phase commit, replayed against
all three recordings by bb test: the instrumented ones through
annotations, Choreo's own through a "step" adapter.examples/two-phase-commit/, self-contained like the other four:
check, check-run of commitTest, and a broken participant that ignores
an abort once it has voted.Done when: bb test replays a recorded trace of each route against a
Clojure two-phase commit with no Quint installed; the example is green under
check and check-run against the working tree; its broken participant fails
naming the transition, the node and the diverging stage; and a driver that
forgets :state-path fails at decoding instead of passing.
— Done. choreo_test.clj replays all four recordings with no Quint, and
generates through both routes under bb test:all. The example's broken
participant fails with in spec {:system {"p3" {:stage {:tag "Aborted"}}}}
against in app … "Prepared", naming #'tpc.core/handle-abort!.
"step". Quint
0.32.0's default rust evaluator, writing more than one trace of Choreo's own
spec, labels most initial states "step", with the picks of an attempt that
was never taken. Replay trusts the label, and the as-written route handles
"step", so its adapter was handed the initial state before init ran.
First handled with :backend :typescript; then found in Quint's own
changelog as a bug fixed in 0.33.0 (#2012), which is now the floor —
0014. Replay still trusts the trace.
Recorded as tpc_mislabel_0/1.itf.json.changes_something, prevents them again.
With it, a run ends when the protocol does, which is also what makes
:max-samples useful: Quint writes the longest of its attempts, and 500
attempts for 50 traces put ten commits among them instead of one.:temporal for verify, after review. TLC is the one checker that
accepts a Choreo spec, and Quint 0.33.0's action properties are checked with
it, so verify takes :temporal — under :backend :tlc only, because under
Apalache Quint asks on stdin first and, unanswered, exits 0 having checked
nothing. Recorded with dev/probes/temporal_probe.sh.replay-file on Choreo traces
is covered by the library's own tests.itf reached 339 lines, and after review was split: itf.paths now
reads a decoded state through the three paths, and the ~200-line rule became
a recommendation with reasons recorded. See architecture.md
§3.Can you improve this documentation? These fine people already did:
Claude, Sasha V. Bogdanov & Aleksandr BogdanovEdit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |