Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time in order to specialize that code to the common case and avoid unnecessary overheads. This form of software speculation requires support for deoptimization when some of the assumptions fail to hold. This paper presents a model just-in-time compiler with an intermediate representation that explicits the synchronization points used for deoptimization and the assumptions made by the compiler’s speculation. We also present several common compiler optimizations that can leverage speculation. The optimizations are proved correct with the help of a proof assistant. While our work stops short of proving native code generation, we demonstrate how one could use the verified optimization to obtain speed up in an end-to-end setting.