# Victoria v0.2.0 - Table of Contents

> Formal-model-driven conformance testing for Elixir implementations using TLA+ traces generated by Apalache.

## Pages

- [Victoria](readme.md)
- [Changelog](changelog.md)
- [Glossary](context.md)

## Modules

- Core verification
  - [Victoria](Victoria.md): The primary API for verifying one fixed formal trace.
  - [Victoria.Model](Victoria.Model.md): Defines the implementation lifecycle used while replaying a trace.
  - [Victoria.Runner](Victoria.Runner.md): Sequentially replays a validated trace through a `Victoria.Model` lifecycle.
  - [Victoria.Step](Victoria.Step.md): A normalized formal state and the transition that produced it.
  - [Victoria.Trace](Victoria.Trace.md): A decoded ITF trace adapted for Victoria replay.
  - [Victoria.Verifier](Victoria.Verifier.md): Compares expected and observed states using exact Elixir equality (`===`).

- Apalache integration
  - [Victoria.Spec](Victoria.Spec.md): High-level access to Apalachex specification validation.

- Workflow orchestration
  - [Victoria.Workflow](Victoria.Workflow.md): Runs Apalache and verifies every materialized trace against one model.
  - [Victoria.Workflow.Result](Victoria.Workflow.Result.md): Complete result of a successful conformance workflow.
  - [Victoria.Workflow.Verification](Victoria.Workflow.Verification.md): Associates one generated trace with its successful verification report.

- ExUnit integration
  - [Victoria.ExUnit](Victoria.ExUnit.md): ExUnit assertion helpers for Victoria conformance verification.

- Errors
  - [Victoria.Runner.Failure](Victoria.Runner.Failure.md): Structured failure returned by fixed-trace replay.
  - [Victoria.Trace.Error](Victoria.Trace.Error.md): A structured Victoria trace-adaptation error.
  - [Victoria.VerificationFailure](Victoria.VerificationFailure.md): The semantic mismatch returned directly by `Victoria.Verifier.verify/2`.
  - [Victoria.Workflow.Error](Victoria.Workflow.Error.md): A contextual conformance-workflow failure.

- Reports
  - [Victoria.Runner.Report](Victoria.Runner.Report.md): Summary returned after a successful fixed-trace replay.

