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