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

Table of Contents
  1. Download
  2. 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 download KeYmaera X. If you are having difficulties, there is also publicly hosted demo.
  1. Install Java JDK (version 1.8+ recommended)
  2. Download KeYmaera X
  3. Run KeYmaera X either by clicking on the keymaerax.jar file
    or by starting it from command line:
      java -jar keymaerax.jar
  4. The KeYmaera X User Interface will open in your web browser at:
  5. Strongly recommended: Install Mathematica (recommended version 10+)
The error Invalid or corrupt jarfile indicates that you need to upgrade Java JDK to version 1.8+. You can check which version of Java you use by running
  java -version

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.


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 versatile user interface.