[ahelwer]

The term you're looking for is model-based testing, where a formal description of the system is used to generate sequences of events which are fed as input to the system under test; the SUT state is then checked for equivalence to the model state. There is significant overlap in concept between model-based testing, property-based testing, and fuzzing: all involve the structured (some more, some less) generation of random inputs to a SUT and the checking of SUT behavior against an assumed-correct oracle. This spans from feeding random system files to the program to see whether it crashes with a strange exception, to a more formalized process directed by a TLA+ (or other language) spec as you've described.

[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.