welcome to the list, and it looks like you did a great job using PBT, and Hypothesis in particular. As to comparing Hypothesis (about which I know next to nothing) and TLA+, I believe that the comment  sums it up pretty well. TLA+ is intended for modeling and analyzing designs at a high level of abstraction, and the Die Hard puzzle just scratches the surface because there is not a lot to abstract from. TLA+ encourages you to abstract from real-world data structures (lists, heaps, priority queues, balanced trees or whatever) and replace them by mathematical concepts, in particular sets and functions. The most convincing use case for TLA+ is for modeling designs before you write any code.
The encouraging observation is that there is a convergence with high-level programming languages and their APIs that encourage you to think in terms of high-level concepts as well, before you commit to any specific implementation for efficiency's sake. I have no idea to what extent the Hypothesis system supports those APIs directly, but if it doesn't, I am confident that it or similar systems will go there at some point.
Personally, I don't think the "concurrency" aspect plays a big role here: note that TLA+ (unless other formalisms such as process algebras) does not have explicit constructs for concurrency but uses non-determinism, just like you state several "rules" in Hypothesis. (You cannot state fairness assumptions in PBT, but that's an advanced subject that is not as immediately relevant as safety properties are.)
My 2 cents,