[romac]

You can also go the other way around and generate traces [1] from the TLA+ or Quint [2] specs using the Apalache model checker [3], map each action in the trace to an action on your system under test, and check that the abstract and concrete states match at each step.

[1] https://apalache-mc.org/docs/adr/015adr-trace.html

[2] https://quint-lang.org

[3] https://apalache-mc.org