[romac]

If you haven't seen those already, you might also want to check out:

  - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
  - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)

[baq]

Quint looks great, thanks for the link!