Are there any proof assistants which integrate JITs?

Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming?

Whilst it may seem like doing so increases the risk of letting incorrect proofs through in complicated JIT implementations, perhaps there's value in faster feedback, with a slower more careful pass always something that could be done later.

What is known about the intersection between these spaces?

• IIRC Lean has this for tactics Feb 9, 2022 at 3:04
• Idk if Coq native_compute counts Feb 9, 2022 at 3:04

• mlang: they elaborate the surface syntax and compile to HOAS, where binding structures are turned into JVM bytecode (see PlatformEvaluator.platformEval). Andras Kovacs said it's supposed to be "always faster". Unlike Lean 4 who JITs only tactics, mlang JITs all bindings.
Coq's native_compute will invoke a modified version of ocamlc to just-in-time compile code for native evaluation. Similarly, vm_compute JITs code to be run by a bytecode interpreter. Both of these are for performance, though often the overhead of compiling to native code dwarfs the time spent running, to the point that native_compute is often slower than vm_compute.