KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

Table of Contents
  1. Overview
    1. Proof Overview
    2. Interactive Proofs
    3. Tactical Proofs
  2. Tool Architecture
  3. Abstract
Download or consult
API Doc or study
Source

Overview

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 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.

Proof Overview

 

KeYmaera X stars in a tutorial video on YouTube
A screenshot of the user interface of the KeYmaera X theorem prover for hybrid systems

Interactive Proofs

A screenshot showing the interactive proof rule application in KeYmaera X

Tactical Proofs

A screenshot showing in-place tactics for tactical proof search in KeYmaera X

Tool Architecture

KeYmaera X was designed to achieve powerful automation of hybrid systems theorem proving while ensuring soundness. The architecture of KeYmaera X is separated into a small, soundness-critical kernel and an extensive tactic framework to regain and exceed the convenience of powerful proof rules.
KeYmaera X is powered by multidynamics technology.

Abstract

KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.

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. Early experimentation with KeYmaera X suggests that a single layer of tactics on top of the axiomatic core provides a rich language for implementing novel and highly sophisticated automatic proof procedures.