[hwayne]

You can use the TLA+ spec to generate a test suite: https://arxiv.org/abs/2006.00915