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.3.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"

For formal verification:

quint_verify "counter invariant",
  invariant: "counter >= 0",
  max_steps: 10

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, test, and verify.
:n_threads	Threads for the Quint Rust backend.
:invariant	Single invariant expression/name for quint run or verify.
:invariants	Invariant names for quint run --invariants or verify --invariants.
:temporal, :inductive_invariant	Temporal and inductive properties for quint verify.
:random_transitions, :apalache_config, :tlc_config, :apalache_version, :server_endpoint	Advanced quint verify options.
: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.