KeYmaera X
KeYmaera X

Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and should therefore strive for highest safety standards - mathematical correctness proof. Proofs for such cyber-physical systems can be constructed with the KeYmaera X prover. As a hybrid systems and hybrid games theorem prover, KeYmaera X analyzes a control program/control policy and the physical behavior of the controlled system together. KeYmaera X supports high assurance by isolating its soundness-critical reasoning in a core of 2000 lines of code. Such a small and simple prover core makes it much easier to trust verification results. Pre-defined and custom tactics built on top of the core drive automated proof search as well as associated verification techniques (e.g, ModelPlex verified runtime monitor synthesis, component-based verification). KeYmaera X comes with a Scala API, a command-line interface, and web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity.

Keywords: Hybrid systems, hybrid games, theorem proving, differential dynamic logic


This work is supported in part by the  DARPA Assured Autonomy  program.


Carnegie Mellon University, Pittsburgh, Pennsylvania, USA


André Platzer

Stefan Mitsch