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