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
Tutorial

Quickly

 ⇓ Download ⇓    KeYmaera X   Documentation     Try Online 

Installation

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. x86-64 CPU such as in Intel/AMD).
  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:
      http://localhost:8090/
  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 for x86-64 CPU such as in Intel/AMD)
    2. Free alternative: Install Wolfram Engine version 12.0 (for x86-64 CPU such as in Intel/AMD. 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
If you are having difficulties, there is also a publicly hosted but slower online demo where you can try out KeYmaera X without installing it.

News

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.