With TLA+, you could check a compiler's specification before you implement it. Then, once you've implemented it, you could do fuzzing on the actual program.
I wonder how much overlap there is between bugs you could catch with TLA+ vs fuzzing.
For example, if I get an error with TLA+--e.g. some state reaches deadlock, or there's an invariant that's violated by some behavior--it takes me a good deal of interpretation to see if there's actually a problem, or if just need to update my spec.
With fuzzing, it seems like the errors would be pretty clear to interpret. e.g. uncaught exceptions, or out-of-bounds memory accesses are clear problems with an implementation, and I would think takes less interpretation.
This is blackbox, so it doesn't allow one to start from nothing as a greybox fuzzer would.
Anyway, testing is not like programming in that different approaches are incompatible. Different testing approaches typically have different blind spots, so they complement each other.