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

  1. KeYmaera X
  2. >>
  3. Install
Table of Contents
  1. Quickly
  2. Installation
  3. Startup Issues
  4. News
  5. Older News and Older Versions
⇓ Download ⇓ or get
Source and read
Book and watch
Videos and follow


 ⇓ Download ⇓    KeYmaera X   Documentation 


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

macOS logo        Linux logo        Windows logo
Startup Issues

  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. JDK for x86 CPU architecture is strongly recommended for Mathematica compatibility, e.g., first install JDK 1.8 version 351 then update it).
  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-13 for x64 CPU architecture but ARM Mathematica should work)
    2. Free alternative: Install Wolfram Engine version 12+ (for x64 CPU architecture but ARM Wolfram should work. Needs active internet and periodic manual license reactivation)
    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.