4 ms·

I've never did that before but this recent post from mongodb team has a interesting view on this. https://www.mongodb.com/blog/post/engineering/conformance-che

• romac 1y ago
  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 https://apalache-mc.org/docs/adr/015adr-trace.html [2] https://quint-lang.org https://quint-lang.org [3] https://apalache-mc.org https://apalache-mc.org