Hypothesis is really a neat library. You can use it to implement stateful testing, which allows you to cover some of the more complex problems that might normally require something like TLA+.

I saw a solution to the water jug problem from the movie Die Hard 3 written in TLA+ and ported it to Hypothesis [0]. It was surprisingly straightforward and easy to read.

[0]: https://nchammas.com/writing/how-not-to-die-hard-with-hypoth...