[berlinquin]

Thanks for naming "model-based testing"--added to my vocabulary. I was thinking more about this, and I would expect very little overlap in the bugs that you could expect to catch with model-based testing 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.