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

Table of Contents
  1. Download
  2. News
Download 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. Open the KeYmaera X User Interface from your web browser
  5. The initialization might take a moment during the first two launches.
  6. Optional: Install Mathematica (not necessary, version 10+ recommended)
  7. Optional: Help->Backend Tool Configuration selects which arithmetic tool to use.
If you see the error Invalid or corrupt jarfile, then you need to upgrade Java JDK to version 1.8+. You can check which version of Java you use by running
  java -version
Instead of upgrading (which is recommended), you can also try to run it via
  java -Xss20M -cp keymaerax.jar KeYmaeraX


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.