One might argue that verifying the correctness of a JIT is basically the same problem as verifying the correctness of an entire compiler, with the added caveat that malicious inputs to the JIT are expected whereas malicious inputs to a compiler might be seen as rare.

IIRC rustc still has a couple of known soundness bugs, for example. It’s only been a few weeks since someone managed to exploit Lean, and Lean is all about formalizing things :)