The prevalence of dynamic languages is not commensurate with the security guarantees provided by their execution mechanisms. Consider, for example, the ubiquitous JavaScript case: it runs everywhere and its complex just-in-time compilers produce code that is fast and, unfortunately, sometimes incorrect.

We present an Isabelle/HOL formalization of an alternative execution model—optimizing interpreters—and mechanically verify its correctness. Specifically, we formalize advanced speculative optimizations similar to those used in just-in-time compilers and prove semantics preservation. As a result, our formalization provides a path towards unifying vital performance requirements with desirable security guarantees.