quint-connect

Model-based testing for Clojure, driven by Quint specifications.

Status: 0.3.0. Every planned milestone in docs/roadmap.md is done — decoding, replay, the annotation registry, the Quint CLI, the public API, failure artifacts, scripted runs and verify. bb test runs a real model-based test end to end, needing no Quint. What is still rough is listed honestly in getting-started.

What it does

You write a formal spec of your system in Quint. Quint generates traces from it (sequences of state -> action -> state). quint-connect starts your application, replays those traces against it, and fails the test at the first step where the application's state diverges from the specification's state.

spec.qnt  --quint run --mbt-->  ITF traces  --replay-->  your running app
                                                  |
                                            state diff on divergence

The mapping between spec and code is declared with metadata, next to the code it describes. The application never learns that Quint exists: no context argument, no return-value convention, no require. This is the Clojure counterpart of quint-connect (Rust).

Coordinates

;; belongs in a :test alias and nowhere else
org.clojars.aldebogdanov/quint-connect {:mvn/version "0.3.0"}

Usage

Annotate the application. The keys are plain keywords needing no require, so an annotated namespace takes on no dependency — this library belongs in your :test alias and nowhere else. Actions take the nondet picks Quint made, bound by parameter name, and their return value is ignored:

(ns bank.core)                                        ; no :require, no deps

(def ^{:quint/state :balances} accounts (atom {}))

(defn deposit
  {:quint/action "deposit"}
  [who amount]
  (swap! accounts update who (fnil + 0) amount))

(defn withdraw
  {:quint/action "withdraw"}
  [who amount]
  (when (>= (get @accounts who 0) amount)
    (swap! accounts update who - amount)))

State is read back from whatever declares itself as state — an atom, a ref, or a getter function. Getters can live in the test namespace when the application has none of its own:

(ns bank.model-test
  (:require [bank.core :as bank]
            [clojure.test :refer [deftest]]
            [org.clojars.aldebogdanov.quint-connect.core :as q]    ; the API
            [org.clojars.aldebogdanov.quint-connect.test :as qt])) ; the bridge

(defn last-error                             ; called with no arguments
  {:quint/state :lastError}
  []
  (bank/current-error))

(defn reset-app {:quint/init true} []   ; runs once per trace, before step 0
  (reset! bank/accounts {"alice" 0 "bob" 0}))

(q/defdriver bank
  {:spec "spec/bank.qnt"
   :main "bankTest"
   :scan '[bank.core bank.model-test]        ; namespaces to read annotations from

   ;; anything that is not one function call goes here, and wins on conflict
   :actions {"transfer" (fn [{:keys [from to amount]}] ...)}})

(deftest bank-conforms-to-spec
  (qt/check bank {:traces 50 :max-steps 20 :seed 42}))

Careful — this is the one syntax trap. Metadata must sit on the symbol or in the attr-map, never on the (defn ...) form:

(defn ^{:quint/action "deposit"} deposit [who amount] ...)  ; works
(defn deposit {:quint/action "deposit"} [who amount] ...)   ; works
^{:quint/action "deposit"} (defn deposit [who amount] ...)  ; SILENTLY IGNORED

q/check is an ordinary function returning ordinary data, so it works from the REPL, from clojure.test, from Kaocha, or from anything else. qt/check is the one-line bridge that turns that data into an assertion.

When the implementation diverges, that assertion fails with:

spec and implementation diverged on trace 0 of 5, seed 42
diverged at step 6, action "deposit"
  picks    {:amount 11, :who "alice"}
  handler  #'bank.core/deposit
  readers  {:balances #'bank.core/accounts}
  expected {:balances {"alice" 11, "bob" 0}}
  actual   {:balances {"alice" 12, "bob" 0}}
  in spec  {:balances {"alice" 11}}
  in app   {:balances {"alice" 12}}
  saved      test-resources/quint-connect/failures/bank-seed42-trace0.itf.json
  reproduce  cd spec && quint run bank.qnt --mbt --seed=42 ...

The handler and reader vars are the payoff of declaring the mapping next to the code: the failure points at the function that diverged and at the one that observed it. The reproduce line is pasteable.

The trace outlives the run

That saved line is a random trace made permanent. Move it out of the gitignored drop zone, commit it, and name it in a test:

(deftest deposit-is-not-off-by-one              ; the bug of 2026-08-17
  (qt/replay-file bank "test-resources/quint-connect/bank-seed42-trace0.itf.json"))

That test needs no Quint, no randomness and no seed: it replays exactly the interleaving that broke you, in milliseconds, in CI. The workflow is docs/getting-started.md §6.

About the keys

Five keys, qualified by quint, requiring nothing: :quint/action, :quint/args, :quint/state, :quint/init, :quint/halt. A sixth, :quint/driver, exists only for the case where one namespace serves two specs and each wants its own lifecycle:

(defn open-ledger! {:quint/init true :quint/driver :ledger} [] ...)
(defn open-cache!  {:quint/init true :quint/driver :cache}  [] ...)

(q/defdriver ledger {:name :ledger :spec "spec/ledger.qnt" :scan '[app.system]})

An annotation without it belongs to every driver, so you can ignore the key until you need it. See docs/decisions/0009-driver-scope.md.

quint is a shared keyword namespace and the Quint project's name, not ours, so a driver can move the whole vocabulary out of the way:

(q/defdriver bank
  {:spec   "spec/bank.qnt"
   :scan   '[bank.core]
   :key-ns 'acme.mbt})          ; now reads :acme.mbt/action, :acme.mbt/state, …

:key-ns moves all six keys together; there is no per-key override and no second spelling within one driver. Note the sharp edge: if you set :key-ns and leave an annotation on :quint/*, nothing reads it and nothing warns you, unless the whole namespace scans empty. See docs/decisions/0007-annotation-keys.md.

Examples

examples/counter/ is the getting-started tutorial as a runnable project — start there. examples/lru/ is a small LRU cache with a bug that only shows up after a particular interleaving of reads and writes, which is the kind of test nobody writes by hand.

cd examples/counter && clojure -M:test

Requirements

• Clojure 1.12+ on the JVM. ClojureScript is out of scope (decision).
• Quint on PATH for trace generation (developed against 0.32.0). Trace replay needs nothing but Clojure — cached ITF files run in CI without Quint installed.
• Apalache (fetched by quint verify) only for the verification mode.

Repository layout

src/org/clojars/aldebogdanov/quint_connect/   library code (.clj)
test/org/clojars/aldebogdanov/quint_connect/  tests
test-resources/quint-connect/  traces promoted from a failing run
examples/counter/              the getting-started tutorial, runnable
examples/lru/                  runnable example: an LRU cache
dev/bank/                      annotated toy implementation of bank.qnt
dev/fixtures/                  example Quint spec + recorded ITF traces
dev/probes/                    scripts that verified the claims in the docs
docs/architecture.md
docs/roadmap.md
docs/decisions/                ADRs — why the design is what it is
docs/notes/                    observed behaviour of Quint and of var metadata
CLAUDE.md                      working agreement for AI-assisted changes

Contributing

See CONTRIBUTING.md. bb test needs nothing but Clojure; bb test:all additionally needs quint on PATH.

License

Copyright © 2026 Michelada

Distributed under the Eclipse Public License 2.0, the same license as Clojure itself.