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.1.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.1.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 release-readiness CI runs on Ubuntu. Other operating systems are not release-tested and Windows support is not claimed.

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, Victoria.ITF.Error when loading fails, 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 lexical artifact-path order, 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. Victoria never empties, reuses, or automatically removes it. victoria-run.json is written as running before Apalache starts and atomically replaced with a completed manifest after materialization succeeds or fails. A process interruption can therefore leave a retained running manifest; Victoria does not recover or resume it.

The manifest records absolute spec/config paths, the executable path, working and run directories, complete argv, exit status, ordered relative trace paths, and a bounded output diagnostic. Do not place secrets in paths or command options. The public Victoria.Apalache.Result retains complete raw subprocess output bytes. Human-readable errors and manifests retain only a binary-safe tail of at most 4 KiB plus byte-count and truncation metadata.

Only top-level regular .itf.json files are materialized; symlinks and nested files are ignored. A nonzero Apalache exit can still be a successful materialization when one or more valid traces were produced. Trace loading is all-or-nothing.

Lower-level APIs

Advanced callers may explicitly compose:

Victoria.Spec
  → Victoria.Apalache.RunDirectory
  → Victoria.Apalache.Plan
  → Victoria.Apalache.run/2
  → Victoria.Apalache.Result
  → Victoria.verify/2

Use these APIs when the caller must own the run path or separately inspect materialization before deciding which traces to verify.

Known limitations

Only Apalache v0.58.3 is supported.
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.
ITF tagged-value support is intentionally partial.
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