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/
├── 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)
├── 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.