Concolic testing would probably catch it, but only if the person that implemented the hardware model for the theorem prover understood the Intel documentation, which seems unlikely.

Basic fuzzing probably wouldn’t catch this; as the other comments point out, the search space is probably too large, and the set of vulnerable executions is probably too small for an undirected random search.