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 and Older Versions
⇓ Download ⇓ or try
Online or get
Source and read
Book and watch
Videos and follow


 ⇓ Download ⇓    KeYmaera X   Documentation     Try Online 


KeYmaera X should run out-of-the-box on macOS or Linux or Windows after you install it.

macOS logo        Linux logo        Windows logo

  1. Install Java Runtime Environment 1.8-1.13 or Java JDK by Oracle or OpenJDK (recommended version 1.8 or 1.13 but intermediate versions are possible).
  2. Download KeYmaera X
  3. Run KeYmaera X either by clicking on the keymaerax.jar file
    or by starting it from command line, which shows startup information:
      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 that you can configure in KeYmaera X→Preferences:
    1. Best functionality: Install Mathematica (version 10-12.0)
    2. Free alternative: Install Wolfram Engine version 12.0 (needs active internet)
    3. Built-in: Z3 Solver (less functionality)
    4. Optional add-on: Install and link both Mathematica and MatLab to improve KeYmaera X invariant generator Pegasus.
    Only unusual use cases need advanced configuration in KeYmaera X→Preferences→Advanced.
  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, please contact Carnegie Mellon University's Center for Technology Transfer and Enterprise Creation.

Building Instructions

Startup Issues

KeYmaera X should run out-of-the-box on most macOS, Linux, or Windows systems (although Windows has been tested less). But depending on your system configuration, some issues can come up.

Startup Issues


KeYmaera X surpasses its predecessor KeYmaera 3 in almost every respect. For example, it provides significantly more sophisticated automatic ODE invariant generation and provides user-defined tactics enable custom proof search procedures. KeYmaera X also comes with a significantly easier yet more versatile user interface. Above all, KeYmaera X has a substantially smaller soundness-critical prover core.

Recent news:

Older News and Older Versions

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

Archive of older releases of KeYmaera X since 2015.