What I ended up doing was essentially reimplementing TLA+ (and TLC) so that I could code-gen runtime tests from my specs. My TLC implementation enables the "nor

What I ended up doing was essentially reimplementing TLA+ (and TLC) so that I could code-gen runtime tests from my specs. My TLC implementation enables the "normal" TLA+-style offline checks to determine that you won't violate your invariants, so you can iterate on your specs and find the edges (and fix them). I do the online checks because I don't trust the code, so I check (at runtime) that the code matches the specIfor the exact (runtime) situation that code is being run in. If it doesn't, I hang/abort.