KeYmaera X Verification

We turn to proof assistants when we need maximum certainty in an answer. For example, we turn to KeYmaera X to ascertain the safety of life-critical cyber-physical systems. But proof assistants are themselves vulnerable to bugs, both in the design of the underlying logic and its realization as a program. Where do proof assistants turn to establish confidence in themselves?

During my PhD, I was the main student on the Verified KeYmaera X project, which answered this question for KeYmaera X. My Isabelle formalization covers the soundness proof for the underlying theory behind KeYmaera X, as does the accompanying Coq Formalization by my collaborators, Vincent Rahli, Ivana Vukotic, and Marcus Voelp. These results are presented in our CPP '17 paper: Formally Verified Differential Dynamic Logic.

A proof term exporter and verified checker built by extending this formalization have successfully been used to check system safety proofs in the PLDI paper.