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) -

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)