We have extended the verified CakeML compiler with a new language primitive,
Eval, which permits evaluation of new CakeML syntax at runtime. This new
implementation supports an ambitious form of compilation at runtime and dynamic
execution, where the original and dynamically added code can share
(higher-order) values and recursively call each other. This is, to our
knowledge, the first verified run-time environment capable of supporting a
standard LCF-style theorem prover design.

Modifying the modern CakeML compiler pipeline and proofs to support
a dynamic computation semantics was an extensive project. We review the
design decisions, proof techniques, and proof engineering lessons
from the project, and highlight some unexpected complications.