  We want to verify the correctness of optimization phases in the GraalVM
compiler, which consist of many thousands of lines of complex Java code
performing sophisticated graph transformations. We have built high-level models
of the data structures and operations of the code using the Isabelle/HOL
theorem prover, and can formally verify the correctness of those high-level
operations. But the remaining challenge is: how can we be sure that those
high-level operations accurately reflect what the Java is doing? This paper
addresses that issue by applying several different kinds of differential
testing to validate that the formal model and the Java code have the same
semantics. Many of these validation techniques should be applicable to other
projects that are building formal models of real-world code.
