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.