Source and read
Book and watch
Videos and follow
- KeYmaera X 4.9 major release with restructured tactic framework and module separation. Model organization, shortcut notation in user definitions, improved support for starting and checking lemmas. (release notes)
- KeYmaera X 4.8 major release with more speed, more automation, restructured and reviewed microkernel, user definitions and more (release notes)
- New KeYmaera X Tutorial
- Best Tool Paper Award at FM 2019 was awarded for Pegasus, the continuous invariant generator for KeYmaera X
- FM 2019 Tutorial on KeYmaera X: Modular Formal Verification of Cyber-Physical Systems with KeYmaera X
- New video lectures: Logical Foundations of Cyber-Physical Systems
- New textbook: Logical Foundations of Cyber-Physical Systems, Springer, 2018
Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and therefore should strive for nothing but the 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 the control program and the physical behavior of the controlled system together.
KeYmaera X features a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning. 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. KeYmaera X comes with a web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity.
- ⇓ Download KeYmaera X to your computer (installation instructions)
- Get KeYmaera X Source to contribute
KeYmaera X is a theorem prover for
KeYmaera X is built up from a small trusted core. The core contains a finite list of locally sound dL axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning in this axiomatic core obviates the otherwise intractable task of ensuring that proof search algorithms are implemented correctly. This enables advanced proof search features---such as aggressive, speculative proof search and user-defined tactics built using a flexible tactic language---without correctness concerns that could undermine the usefulness of automated analysis. KeYmaera X demonstrates that tactics on top of the axiomatic core provide a rich language for implementing novel and highly sophisticated automatic proof procedures.
Case StudiesThese are a few of the many other case studies that have been verified in KeYmaera X:
Other case studies are reported in corresponding publications.
Also get quick usage help any time with themenu button in KeYmaera X.
Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.