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

romac 8 months ago | parent | context | favorite | on: Re-fixing Servo's event-loop

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 8 months ago [–]

Quint looks great, thanks for the link!