This work-in-progress report presents ongoing experiments relating to formal verification of JIT compilers for language VMs. The native CPU code of the VM — which consists of statically-known code and variable output of the JIT — is executed in a symbolic simulation engine. This simulation yields identities that hold over the total range of inputs (or disproves them by providing a counterexample).

One obstacle we had to overcome, is executing CPU code which is itself symbolic, i.e. given as formulae over input variables. To solve this problem, we designed a new ISA-agnostic translator from ISA-specific binary machine language into an intermediate language which can be directly simulated by the symbolic engine.