Victoria

Victoria connects formal TLA+ execution traces to concrete Elixir implementations. It can replay committed ITF traces or invoke Apalache to generate traces and verify an implementation against every generated behavior.

Status

Victoria 0.2.0 is experimental. The two core workflows are usable, but public APIs may change during the 0.x series and Apalache compatibility is intentionally narrow.

Installation

Add Victoria to mix.exs:

def deps do
  [
    {:victoria, "~> 0.2.0"}
  ]
end

Requirements

Fixed-trace verification requires Elixir 1.18 or later and does not require Apalache.

Generated workflows require Elixir 1.18 or later, Apalache exactly v0.58.3, and Apalache's Java and solver runtime prerequisites on the test process's PATH. Victoria's CI runs on Ubuntu. Other operating systems are not CI-tested and Windows support is not claimed.

Development

Victoria uses asdf 0.16.5 and the exact tool versions declared in .tool-versions. Install the complete toolchain with just setup, verify the active tools with just doctor, and fetch project dependencies with just deps. Run the ordinary test suite with just test or the full quality gate with just check.

CI uses pinned, purpose-built setup actions that read the same .tool-versions file. Local tool installation remains owned by asdf through just setup.

Use just --list to see the focused documentation, package, consumer, and real-Apalache checks used by CI.

Model callback contract

A model owns the lifecycle of the implementation being checked:

defmodule Counter.Model do
  @behaviour Victoria.Model

  @impl true
  def init(%{"count" => count}), do: Agent.start_link(fn -> count end)

  @impl true
  def execute(%Victoria.Step{action: "Increment"}, counter) do
    Agent.update(counter, &(&1 + 1))
    {:ok, counter}
  end

  def execute(%Victoria.Step{action: "Decrement"}, counter) do
    Agent.update(counter, &(&1 - 1))
    {:ok, counter}
  end

  @impl true
  def snapshot(counter), do: %{"count" => Agent.get(counter, & &1)}

  @impl true
  def project(%Victoria.Step{state: state}), do: state

  @impl true
  def cleanup(counter), do: Agent.stop(counter)
end

The impl returned by init/1 and threaded through execute/2 is an opaque implementation value owned by the model. It may be a value, PID, database context, client, or another implementation handle.

init/1 creates the implementation from formal state zero.
execute/2 applies each later formal action and returns the next implementation handle.
snapshot/1 returns the implementation's observed state.
project/1 returns the formal step's expected state.
Optional cleanup/1 releases resources once after successful initialization on every controlled exit.

State zero is initialized and verified but never executed.

Fixed-trace verification

Load a committed ITF trace and verify it programmatically:

{:ok, trace} = Victoria.Trace.load("test/traces/counter.itf.json")
{:ok, report} = Victoria.verify(Counter.Model, trace: trace)

# A path may be supplied directly too.
{:ok, report} = Victoria.verify(Counter.Model, trace: "test/traces/counter.itf.json")

Or use the ExUnit assertion:

import Victoria.ExUnit

:ok = assert_conform(Counter.Model, trace: "test/traces/counter.itf.json")

Victoria.verify/2 returns a Victoria.Runner.Report on success, an upstream ITF.Error for generic file, JSON, or ITF failures, Victoria.Trace.Error for Victoria adaptation failures, or Victoria.Runner.Failure when replay fails. The assertion converts controlled failures to ExUnit.AssertionError; programmer misuse remains ArgumentError.

Generated conformance workflow

Create a validated spec and let Victoria allocate a run, invoke Apalache, and verify every trace:

{:ok, spec} =
  Victoria.Spec.new(
    source: "test/specs/Counter.tla",
    config: "test/specs/Counter.cfg"
  )

{:ok, result} =
  Victoria.Workflow.run(
    Counter.Model,
    spec,
    plan: [mode: :simulate, length: 10, max_run: 5]
  )

The ExUnit form runs the same workflow:

import Victoria.ExUnit

:ok =
  assert_conform(
    Counter.Model,
    spec,
    plan: [mode: :simulate, length: 10, max_run: 5]
  )

Generated traces are verified sequentially in the order supplied by Apalachex, without deduplication. Every trace gets a fresh model lifecycle and verification stops on the first failure.

Verification semantics

For the initial state and after every executed step, Victoria performs exactly:

expected = Model.project(step)
observed = Model.snapshot(impl)
expected === observed

Victoria does not calculate business outcomes in Elixir. The TLA+ trace supplies expected behavior and the model exposes the corresponding implementation state. A mismatch returned directly from Victoria.Verifier.verify/2 is a public Victoria.VerificationFailure; replay wraps that semantic mismatch with lifecycle context in Victoria.Runner.Failure.

Artifacts and execution behavior

Generated workflows allocate an exclusive run directory below tmp/victoria by default. Its name contains one UTC timestamp, the TLA+ source basename, and a random six-character hexadecimal suffix. The artifacts: [root: path] workflow option selects another root.

The run directory is retained on success and failure. Apalachex exclusively reserves it and neither Apalachex nor Victoria empties, reuses, or automatically removes it. Apalachex writes apalachex-run.json as running before Apalache starts and atomically replaces it with a completed execution manifest after artifact discovery succeeds or fails. A process interruption can therefore leave a retained running manifest; neither library recovers or resumes it.

The manifest records absolute spec/config paths, the executable path, working and run directories, complete argv, exit status, ordered relative ITF paths, and a bounded output diagnostic. Do not place secrets in paths or command options. Victoria.Workflow.Result.apalache is an Apalachex.Result and retains complete raw subprocess output bytes and ordered itf_paths; it does not contain loaded traces. Human-readable errors and manifests retain only bounded, binary-safe diagnostics.

Apalachex materializes only top-level regular .itf.json files; symlinks and nested files are ignored. A nonzero Apalache exit can still be a successful materialization when one or more artifacts were produced. Victoria then loads those paths in order. The standalone ITF package owns format decoding, while Victoria owns semantic adaptation and replay. Victoria trace loading is all-or-nothing, and apalachex-run.json truthfully remains materialized if Victoria later rejects an invalid ITF. Victoria does not write or rewrite a second manifest.

Lower-level APIs

Advanced callers can use the Apalachex 0.1.x API directly:

Victoria.Spec.new/1 → Apalachex.Spec
  → Apalachex.RunDirectory.build/2
  → Apalachex.Plan.new/2
  → Apalachex.run/2
  → Apalachex.Result.itf_paths
  → Victoria.Trace.load/1
  → Victoria.verify/2

The low-level Victoria.Apalache modules and Victoria.ITF were removed during the direct 0.x dependency boundary cleanup. Victoria.Spec.new/1 now returns Apalachex.Spec and preserves Apalachex.Spec.Error unchanged.

Known limitations

Apalachex 0.1.x supports only Apalache v0.58.3.
Apalache execution is synchronous and has no Victoria timeout.
Cancellation and caller-death handling are not implemented.
Lasso traces can be materialized but cannot be replayed.
State comparison uses exact Elixir ===.
Generated traces are verified sequentially.
Generated verification stops on the first failing trace.
Apalache run artifacts are retained automatically.
Public APIs may change during the 0.x series.

License

Victoria is available under the MIT License.

Next Page → Changelog