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.
If you are interested in TLA+, you might want to check out Quint (https://quint-lang.org), a modern take on a specification language which shares the same underlying temporal logic of actions, but with a syntax more familiar to programmers.
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)
Vale has a very interesting approach to memory safety, without garbage collection or a borrow checker, using a memory management technique called "generational references" which I had never heard of previously.