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?
I lead the Verified KeYmaera X project, which answers 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.
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer.
VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models.
Programming Language Design and Implementation - 39th ACM SIGPLAN Conference,
PLDI 2018, Philadelpha, PA, June 18-22, 2018, ACM, 2018. © ACM. To appear. draft
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer.
Formally verified differential dynamic logic.
Certified Programs and Proofs - 6th ACM SIGPLAN Conference,
CPP 2017, Paris, France, January 16-17, 2017, ACM, 2017. © ACM