Glad you have tried FizzBee before. Do you have any feedback on it? With TLA+, I mostly see papers and example projects that typically implement model based tr

Glad you have tried FizzBee before. Do you have any feedback on it? With TLA+, I mostly see papers and example projects that typically implement model based trace checking solutions in TLA+. While it works, usually, it will clutter the main code (SUT) with tracing library calls. And in some papers, you'll need to create a separate modified version of spec with the tracing spec. MongoDB published a paper a while ago comparing model based testing and model based trace checking. I'll soon list more details.