Yeah I wonder if there has been much work on formal verification here (including of compiler passes). I know the LLVM team have done some interesting work on verifying LLVM passes using the Alive2 tool for example.