quint-connect, model-based testing for Elixir with Quint

Most test suites check examples. You write a function, write tests against the inputs you happened to think of, and ship. The bug you find in production is usually the one you did not think to test, because you cannot remember inputs you did not imagine. Specifications close part of that gap. A spec describes how the system is allowed to behave, and a tool walks the state space looking for behaviour that breaks the description. Different shape of test, different kind of feedback.

This is a small follow-up to the post about Kaizen. This time the subject is quint-connect, a small Elixir library I just published on Hex.

What Quint is

Quint is a specification language built and maintained by Gabriela Moreira and her team at Informal Systems. It is the spiritual descendant of TLA+, with a friendlier surface: an ML-flavoured syntax, real types, and a CLI you can run on your laptop without learning a separate proof language. You write a spec, Quint walks the state space (or samples it with random walks), and emits traces in a stable JSON shape called ITF, the Informal Trace Format.

A minimal Quint module looks like this:

module counter {
  var counter: int

  action init = all {
    counter' = 0,
  }

  action inc = all {
    nondet amount = Set(1, 2, 3).oneOf()
    counter' = counter + amount,
  }

  action step = inc
}

init sets the starting state. step is the transition relation that gets repeated. nondet is a controlled choice; Quint picks one element from the set each step, and the test runs explore those branches. From here, quint run produces sample traces, and quint test checks named properties against many random executions.

Two things matter for what comes next. First, the spec is executable. You can poke it like a regular program before committing to a verification run, which makes it cheap to iterate on. Second, the trace format is stable and language-agnostic. Anyone willing to read ITF can plug their implementation into a trace generated by Quint, without caring how Quint produced it. That seam is exactly where quint-connect lives.

Why Quint pairs with LLM-assisted coding

The interesting thing about specs in 2026 is not the maths. It is the feedback loop they create when a language model is doing most of the typing.

When I ask a model to implement a feature, it produces something plausible. Tests catch the cases I happened to think about. A spec catches the cases I did not. The model writes code; the spec is the contract; Quint walks states and flags drift. If the implementation goes off-script, I get a concrete trace showing exactly which sequence of actions broke an invariant. That trace is short, mechanical, and reproducible, which makes it the kind of feedback weaker models can act on without re-reading the entire codebase.

This is the harness angle I mentioned in the Kaizen post. Specs let me lean on cheaper models like composer 2 or haiku for the bulk of implementation work, because the spec carries the proof and not the prose. I no longer need a senior reviewer to read every diff to feel safe. I need Quint to disagree with the diff, which it does quickly and unsentimentally.

None of this is a claim that formal methods solve LLM correctness. It is a claim that having an executable contract around your code is suddenly cheap, and cheap matters when you are writing more code per hour than you used to.

How quint-connect works

quint-connect is the Elixir sibling of the Rust crate of the same name. It does three things.

First, it shells out to the Quint CLI. The package does not embed Quint; it asks quint run or quint test to produce ITF traces, then reads them back. Keeping Quint at arm’s length means I do not have to track its version inside the Elixir release. As long as quint is on PATH, the package is happy.

Second, it decodes ITF. The package understands the value-oriented JSON Quint emits: integers, bigints, maps, sets, tuples, records, variants. Each step in the trace is exposed as a QuintConnect.Step struct carrying the action name, the nondeterministic picks made along the way, and the post-state from the model.

Third, it replays. You implement two behaviours:

• QuintConnect.Driver translates Quint actions into your implementation. Given a step, return the new state of your code.
• QuintConnect.State (optional) projects your implementation state into a comparable shape, so the package can assert step by step that your code agrees with the spec.

The DSL entry point is a macro on top of ExUnit:

use QuintConnect.Case, spec: "priv/specs/counter.qnt"

quint_run "counter follows the model",
  driver: CounterDriver,
  max_samples: 10,
  max_steps: 20,
  seed: "1"

quint_run generates random traces. quint_test checks a named property. Both fail the ExUnit test if the spec and the implementation disagree on any step.

A worked example

With the spec above, the driver translates each Quint action into a call against your Elixir code. Here is a tiny driver that mirrors the spec inline so the moving pieces stay visible:

defmodule CounterDriver do
  @behaviour QuintConnect.Driver
  @behaviour QuintConnect.State

  alias QuintConnect.Step

  def init(_opts), do: {:ok, %{"counter" => nil}}

  def step(_state, %Step{action_taken: "init"}) do
    {:ok, %{"counter" => 0}}
  end

  def step(state, %Step{action_taken: "inc"} = step) do
    with {:ok, amount} <- Step.nondet(step, :amount) do
      {:ok, Map.update!(state, "counter", &(&1 + amount))}
    end
  end

  def from_implementation(state), do: {:ok, state}
end

The ExUnit case that wires the spec, the driver, and the runner together is small:

defmodule CounterMBTTest do
  use QuintConnect.Case, spec: "priv/specs/counter.qnt"

  quint_run "counter follows the model",
    driver: CounterDriver,
    max_samples: 10,
    max_steps: 20,
    seed: "1"
end

mix test runs Quint, decodes the resulting traces, and replays them. If the driver disagrees with the model at any step, the test fails with the failing step and the projected state diff. The seed is fixed, so any failure is reproducible by design.

To pull the package into your own project, drop this into mix.exs and run mix deps.get:

{:quint_connect, "~> 0.1.0", only: :test}

Design notes

A handful of opinionated calls worth surfacing.

Shells out, not bound. The trade is that you need Quint installed separately (npm @informalsystems/quint). The upside is that Quint upgrades do not force a quint-connect release.

Speaks ITF, not Quint AST. ITF is stable across Quint versions; the AST is not. This is the kind of choice that ages well.

Nondeterministic picks are routed explicitly. Step.nondet/2 forces the driver author to name each choice, which prevents silent mismatches between what the spec branches on and what the driver expects. The test fails loudly when the contract drifts.

ExUnit cases run with async: false. Quint traces are deterministic per seed, but multiple Quint subprocesses fighting for CPU is a recipe for flake. The package errs on the boring side here.

The library is Apache-2.0, fresh on Hex at version 0.1.0, and small enough to read in an afternoon. Contributions and bug reports welcome.

Closing

Quint is a small superpower, and quint-connect is the smallest thing I could ship that lets an Elixir codebase use it for real. If you try it, tell me what broke and what surprised you.

Repo: github.com/marquesds/quint-connect. Hex: hex.pm/packages/quint_connect.

Thanks for reading this post! Bye 👋🏾