Quint Connect for Elixir

quint_connect brings model-based testing with Quint to Elixir projects. It generates ITF traces with the Quint CLI, decodes each trace, and replays the actions against an Elixir driver that wraps your implementation.

This package is an Elixir sibling of the Rust quint-connect crate. It keeps the same Apache-2.0 license and ports the core workflow into idiomatic ExUnit.

Installation

Add quint_connect to mix.exs:

def deps do
  [
    {:quint_connect, "~> 0.2.0", only: :test}
  ]
end

Install the Quint CLI separately:

npm install --global @informalsystems/quint

Requirements:

Elixir 1.19+
Erlang/OTP 28+
Quint available on PATH when running generated traces

Quick Start

Write a driver that translates each Quint action into implementation calls:

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

  import QuintConnect.Step.Switch

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

  def step(state, step) do
    quint_switch step do
      init -> {:ok, %{"counter" => 0}}
      inc(amount) -> {:ok, Map.update!(state, "counter", &(&1 + amount))}
    end
  end

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

For Quint action names that are not valid Elixir identifiers, use string clauses:

quint_switch step do
  "MoveX", [corner?, coordinate?] -> move_x(corner? || coordinate?)
  "MoveO", [coordinate] -> move_o(coordinate)
end

Required picks return {:error, {:missing_nondet, name}} when absent. Optional picks end in ? and bind nil when absent.

Use the ExUnit DSL to generate Quint traces and replay them:

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

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

For Quint test actions:

quint_test "counter property",
  driver: CounterDriver,
  test: "counterWorks",
  max_samples: 10,
  seed: "1"

Driver Contract

The driver init callback creates the implementation state. step/2 receives a QuintConnect.Step with:

action_taken: the Quint action name.
nondet_picks: decoded nondeterministic choices.
state: the comparable model state after metadata is removed and state_path is applied.

If the driver also implements the state projection callback, replay compares the projected implementation state after every step.

Configuration

Common options:

Option	Purpose
`:seed`	Reproduce Quint traces.
`:max_samples`	Number of generated traces.
`:max_steps`	Maximum steps for `quint run`.
`:n_traces`	Number of generated traces when `:max_samples` is absent.
`:main_module`	Quint module passed as `--main`.
`:init_action`	Init action name for `quint run`; defaults to `"init"`.
`:step_action`	Step action name for `quint run`; defaults to `"step"`.
`:backend`	Quint backend for `run` and `test`.
`:n_threads`	Threads for the Quint Rust backend.
`:invariant`	Single invariant expression/name for `quint run`.
`:invariants`	Invariant names for `quint run --invariants`.
`:witnesses`	Witness names for `quint run --witnesses`.
`:hide`	Variable names hidden from terminal output.
`:mbt`	Enables `quint run --mbt`; defaults to `true`.
`:state_path`	Path into model state before comparison.
`:nondet_path`	Path to a custom action record when not using `--mbt`.
`:quint_executable`	CLI executable; defaults to `"quint"`.
`:verbosity`	Quint verbosity; defaults to `0` for subprocess runs.

Environment variables:

Variable	Purpose
`QUINT_VERBOSE`	Default verbosity passed to Quint.
`QUINT_SEED`	Default seed when no `:seed` option is provided.

When neither :seed nor QUINT_SEED is set, Runner generates a seed and passes it to Quint. Replay failures include QUINT_SEED=... reproduction text.

Examples

The priv/examples/ directory includes:

counter.qnt — minimal MBT flow.
tictactoe.qnt — Rust upstream-style game model using optional picks.
two_phase_commit.qnt — compact protocol model with custom nondet_path.

Local Development

Run the normal suite:

mix test

Run tests that require the Quint CLI:

mix test --include quint

The :quint suite includes self-hosted specs under priv/specs/. These specs replay through QuintConnect.Case and validate the package's own CLI and step extraction behavior.

Release checks:

mix format --check-formatted
mix test --include quint
mix docs
mix hex.build

Limitations

ITF decoding covers the value shapes emitted by current Quint traces: bigint, map, set, tuple, records, and variants.
State comparison is exact. Drivers should project implementation state into the same shape as the Quint model.
The package shells out to the Quint CLI; it does not embed Quint.

License

Apache-2.0. See LICENSE.