Thanks a lot. It does handle concurrency.

https://fizzbee.io/testing/tutorials/quick-start/#parallel-t...

Sequential logic is generally easier to test (also concurrency testing of linearizable systems). FizzBee specification language is created primarily to express concurrent behavior of non-linearizable systems - like eventual consistency, etc.

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.

Thanks. Please give it a try, and let me know if you have any issues. I'd be happy to help.