Jitterbug is a framework for writing just-in-time (JIT) compilers and proving them correct. It provides a precise specification of JIT correctness and an automated verification strategy that scales to practical implementations.
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Nov 2020. [pdf] [slides]