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

Table of Contents
  1. Quickly
  2. Installation
  3. Startup Issues
  4. News
  5. Older News
⇓ Download or get
Source or read
Book or watch


 ⇓ Download ⇓     KeYmaera X    Documentation 


KeYmaera X should run out-of-the-box after you install it:
  1. Install Java JDK 1.8 (recommended version 1.8 but versions 1.9-1.10 are possible yet 1.11 is not)
  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. Log in to your KeYmaera X User Interface that will open in your web browser:
  5. The KeYmaera X User Interface will show you different options for arithmetic:
    1. Best functionality: Install Mathematica (recommended version 10+)
    2. Free alternative: Install Wolfram Engine (needs active internet)
    3. Built-in: Z3 Solver (less functionality)
  6. Start exploring KeYmaera X or read quick user guide

KeYmaera X is available as open source under GPLv2. If you prefer to 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 easily definable custom proof search procedures, and more sophisticated ODE invariant generation. KeYmaera X also comes with a significantly more versatile user interface. Above all, KeYmaera X has a substantially smaller soundness-critical prover core.

Older News

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