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
Tutorial

Quickly

 ⇓ Download ⇓    KeYmaera X   Documentation     doi 

Installation

The KeYmaera X aXiomatic Tactical Theorem Prover for Hybrid Systems 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 11+ (tested till Java 22).
  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 the KeYmaera X→Preferences menu:
    1. Best functionality: Install Mathematica (version 10+ for x64 CPU architecture or ARM64 CPU architecture)
    2. Free alternative: Install Wolfram Engine version 12+ (for x64 CPU architecture or ARM64 CPU architecture. 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 the menu KeYmaera X→Preferences→Advanced.
  6. Start exploring KeYmaera X or read user guide.

KeYmaera X is available as open source under GPLv2.

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

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.