- Conformance — agreement between a formal trace and an implementation across all verified states.
- Verification — exact comparison of one expected state with one observed state.
- Expected state — the state described by the formal trace.
- Observed state — the state reported by the implementation.
- Runner — the participant that replays a formal trace against an implementation.
- Verifier — the participant that compares expected and observed states.
- Spec — a validated reference to one TLA+ source artifact and its optional configuration artifact.
- Apalache plan — a non-executing description of a future Apalache operation.
- Apalache execution — synchronous execution of an existing Apalache plan by Apalachex, without Victoria implementation verification.
- Artifact materialization — Apalachex discovery of generated top-level ITF files, recorded independently of whether Victoria can decode them.
- Trace loading — ordered, all-or-nothing decoding of every Apalachex ITF path by the standalone ITF package and semantic adaptation into Victoria traces for replay.
- Supported Apalache version — the exact Apalache release validated by the current Victoria release; Victoria 0.2.0 supports v0.58.3.
- Run directory — the location exclusively reserved by Apalachex for one operation; its artifacts survive successful and failed materialization.
- Run manifest — the Apalachex-owned
apalachex-run.jsondocument recording the plan, execution context, artifacts, and outcome of one Apalache operation. Victoria writes no second manifest. - Running manifest — the initial run manifest committed before Apalache starts, showing that the run was reserved but has not reached a materialized or failed outcome.
- Completed manifest — the final run manifest written after execution and artifact materialization finish.
- Materialized outcome — a completed Apalachex manifest outcome showing that one or more ITF artifacts were discovered, regardless of Apalache's exit status or later Victoria decoding and verification.
- Orphaned run — a retained run directory whose manifest remains
runningbecause its owner did not complete the final manifest replacement. - Atomic manifest replacement — writing a complete temporary manifest and renaming it over the prior manifest so observers never see partially written JSON; this is not a power-loss durability guarantee.
- Successful materialization — a terminated Apalache process for which Apalachex found one or more ITF artifacts, regardless of raw exit status or whether Victoria later accepts their contents.
- Apalache result — an
Apalachex.Resultwith complete execution context and ordereditf_paths. It does not contain Victoria traces. - Conformance workflow — a high-level operation that allocates an Apalache run, loads its materialized artifacts as formal traces, and verifies those traces against an implementation model.
- Workflow verification — the result of verifying one generated trace through an independent implementation lifecycle.
- Stop-first verification — sequential verification that terminates after the first trace that does not conform.
- Completed verification — a successful verification report produced before a later trace failed.
- Workflow success — an Apalache run materialized one or more ITF artifacts, Victoria loaded them as traces, and every trace conformed. The workflow does not deduplicate traces, every trace starts a fresh implementation lifecycle, direct Apalachex lower-level APIs remain independently usable, and no workflow-level durable manifest exists.
- Generated conformance assertion —
Victoria.ExUnit.assert_conform/3runs a complete generated conformance workflow from a validated Spec and raisesExUnit.AssertionErrorwhen controlled Apalache, trace-loading, or implementation-verification failures occur.assert_conform/2remains the fixed-trace form. Both plain functions return only:okon success and preserve programmer misuse asArgumentError; callers needing%Victoria.Workflow.Result{}useVictoria.Workflow.run/3directly.