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.1.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

  alias QuintConnect.Step

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

  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

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`.
`: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"`.
`: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"`.

Environment variables:

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

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.