Install KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

Table of Contents
  1. Installation
  2. Startup Issues
  3. News
  4. Older News
⇓ Download or try
Online or read
Book or list
Documents or consult
API Doc or study


KeYmaera X should run out-of-the-box after you install it. If you are having difficulties, there is also publicly hosted but fairly slow demo.
  1. Install Java JDK (recommended version 1.8 but 1.9-1.10 are possible)
  2. Strongly recommended: Install Mathematica (recommended version 10+)
  3. Download KeYmaera X
  4. Run KeYmaera X either by clicking on the keymaerax.jar file
    or by starting it from command line:
      java -jar keymaerax.jar
  5. Log in to the local KeYmaera X User Interface that will open in your web browser:

KeYmaera X is available as open source under GPLv2. If you would rather use KeYmaera X under another license, just contact Carnegie Mellon University's Center for Technology Transfer and Enterprise Creation.

Startup Issues


KeYmaera X is a stable release surpassing almost all capabilities of its predecessor KeYmaera 3. KeYmaera X provides numerous features that KeYmaera 3 users have been dreaming of for a long time. For example, user-defined tactics and easily definable custom proof search procedures. KeYmaera X also comes with a more versatile user interface.

Older News

Archive of older news since the first public release 04/18/2015.