This is neat. I've used FizzBee and TLA+ for model checking. Being able to test the implementation would be nice.
How is this different from test case generation in TLA+?
Lamport didn't design TLA+ for model checking or for practicing developers to use. He did purely for publishing papers where the researchers express their proofs as math (his new TLA+) instead of free form text.