Verify that your implementation follows the rules defined by a TLA+ model through trace replay over a language-agnostic IPC protocol.

ModelMirrors uses Apalache to generate or load ITF traces from a TLA+ spec, then replays those traces step-by-step against a client process. At each step the mirror compares the client's actual state against the expected state from the trace and reports whether they match.

The mirror runs as a standalone process. Clients communicate with it over stdin/stdout using JSON messages. This means clients can be written in any language — they just need to speak the protocol.

+----------------+     JSON over stdin/stdout     +-----------------+
| Client Process | <----------------------------> | Mirror Process  |
| (your impl)    |                                | (ModelMirrors)  |
+----------------+                                +-----------------+
                                                          |
                                                    +-----+------+
                                                    | Apalache   |
                                                    | (TLA+ spec)|
                                                    +------------+

The mirror validates the spec, generates traces, then replays them:

Client                Mirror
  | --- register --------> |
  |                        | -- validate spec + generate traces
  | <-- spec_validated --- |
  | <-- initial_state ---- |
  | --- report_state ----> |
  | <-- step_ok / mismatch |
  |        ...             |
  | <-- all_steps_done --- |

If you already have ITF traces (e.g. generated offline, or from a previous run), send them directly. The mirror skips Apalache entirely and goes straight to replay:

Client                Mirror
  | -- register_traces --> |
  | <-- spec_validated --- |
  | <-- initial_state ---- |
  | --- report_state ----> |
  |        ...             |
  | <-- all_steps_done --- |

• GHC 9.10+
• apalache-mc on PATH
• cabal (or Bazel 8.7.0)

cabal build all

Or with Bazel:

bazel build //...

cabal run ModelMirrors

The mirror reads a single ClientMessage from stdin, processes it, and writes MirrorMessage replies to stdout.

Example: pipe a Register message to the mirror using your spec file:

echo '{"proto_step":"register","specPath":"test/specs/HourClock.tla","traceConfig":{"invariant":"Inv","lengthBound":3,"numTraces":2,"view":null,"cinit":null,"paramVars":""}}' | cabal run ModelMirrors

Example: pipe a RegisterTraces message with inline ITF traces:

echo '{"proto_step":"register_traces","itfTraces":[...]}' | cabal run ModelMirrors

cabal test all

Tests include integration tests that invoke apalache-mc on test/specs/HourClock.tla. Expect seconds to minutes of runtime.

Language independence is a goal of ModelMirrors. The protocol is the common knowledge shared between client and mirror.

All messages are JSON objects with a "proto_step" field that identifies the message type.

{
  "proto_step": "register",
  "specPath": "path/to/spec.tla",
  "traceConfig": {
    "invariant": "Inv",
    "lengthBound": 5,
    "numTraces": 2,
    "view": null,
    "cinit": null,
    "paramVars": ""
  }
}

{
  "proto_step": "register_traces",
  "itfTraces": [
    {
      "vars": ["x", "y"],
      "param_vars": [],
      "params": [],
      "states": [
        {"action_taken": "init", "x": {"#bigint": "0"}, "y": {"#bigint": "0"}},
        {"action_taken": "inc", "x": {"#bigint": "1"}, "y": {"#bigint": "0"}}
      ]
    }
  ]
}

{
  "proto_step": "report_state",
  "state": {"x": {"#bigint": "1"}, "y": {"#bigint": "0"}}
}

{"proto_step": "spec_validated", "result": "valid"}

{
  "proto_step": "initial_state",
  "action": "init",
  "state": {"count": {"#bigint": "0"}}
}

{
  "proto_step": "next_step",
  "action": "inc",
  "parameters": {"stride": {"#bigint": "2"}}
}

{
  "proto_step": "step_mismatch",
  "expected": {"count": {"#bigint": "1"}},
  "actual": {"count": {"#bigint": "2"}}
}

A client in any language must:

1. Open the mirror as a subprocess (or connect to it via stdin/stdout).
2. Send either a register or register_traces message.
3. Wait for spec_validated.
4. Wait for initial_state to begin a trace.
5. For each next_step, execute the action, then send report_state with the resulting state.
6. Handle step_ok (continue) or step_mismatch (failure).
7. Wait for all_steps_done to signal completion.

See src/Protocol/Client.hs for a reference Haskell client implementation, including cannedClient (pre-canned responses), fixedClient (static state), and hourClockClient (real logic for the HourClock spec).

ModelMirrors verifies its own mirror implementation using model-based testing (MBT). A TLA+ protocol model generates expected action sequences; the real mirror is driven through the same flows and its output is compared.

1. Model the protocol — specs/MirrorProtocol.tla is a state machine with two parties (mirror and client), message channels, and actions like MirrorRecvRegister, MirrorSendInitialState, MirrorRecvReportState. Invariants act as stop conditions — violating them produces counterexample traces.

2. Generate traces — Apalache model-checks the spec. When an invariant is violated, it produces ITF traces — sequences of states showing every action taken. With numTraces = 100, we get distinct protocol flows covering different registration paths, step counts, and Ok/Mismatch branches.

3. Drive the mirror — For each trace, the test forks the real mirror and a real HourClock client (hourClockClient + runClientWithTraces). The client sends a RegisterTraces message with a pre-generated HourClock trace; the mirror replays step-by-step; the client responds with correct state computed via hcTick. The mirror returns a [MirrorStep] — a structured trace of every protocol event it performed.

4. Normalize — MinimalTraceCheck.normalize collapses timing-dependent pairs (RecvReport+StepOk → StepOk, RecvReport+StepMismatch → StepMismatch) and strips terminal AllStepsDone.

5. Build the expected sequence — The TLA+ trace's mirror actions are extracted and normalized to canonical names (e.g. RecvRegister → RecvRegisterTraces since the test always uses that path).

6. Compare — Both sequences are trimmed to the spec's step count and compared with ==. The key insight: step results (StepOk vs StepMismatch) map to the same canonical name — the MBT test verifies protocol message sequence, not state correctness.

ModelMirrors/
├── app/              Executable entry point (stdio mirror)
├── src/
│   ├── Apalache/     Apalache types, command runner, trace parsing
│   ├── Engine/       Trace replay engine and step diffing
│   ├── Protocol/     IPC protocol (core types, JSON format, transport)
│   └── MinimalTraceCheck.hs   Trace normalization and comparison
├── test/
│   ├── Main.hs       Test runner
│   └── specs/        TLA+ specs used by integration tests
├── specs/            Protocol specification (TLA+)
├── docs/             Design documents
├── ModelMirrors.cabal
└── BUILD.bazel

See LICENSE.