How might one automatically check that a formalized theory that is meant to describe a real, physical system actually describes the system in question? For example, if one wishes to reason about Java programs, and one mechanizes a semantics of Java in a theorem prover, how can you be sure that your semantics matches the actual behavior of the Java compiler and virtual machine?