
⇓ Download ⇓
or get Source and read Book and watch Videos and follow Tutorial 
Quickly
Installation
KeYmaera X should run outofthebox on macOS or Linux or Windows after you install it.
 Install Java Runtime Environment 1.81.13 or Java JDK by Oracle or OpenJDK (recommended version 1.8 or 1.13 but intermediate versions are possible).
 Download KeYmaera X
 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
 Log in to your KeYmaera X User Interface that will open in your web browser:
http://localhost:8090/
 The KeYmaera X User Interface will show you different options for arithmetic that you can configure in KeYmaera X→Preferences:
 Best functionality: Install Mathematica (version 1012.0)
 Free alternative: Install Wolfram Engine version 12.0 (needs active internet)
 Builtin: Z3 Solver (less functionality)
 Best functionality: Install Mathematica (version 1012.0)
 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 outofthebox 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 
 On macOS, the error
"keymaerax.jar" cannot be opened because it is from an unidentified developer
indicates that you have to use the Rightclick→Open menu the first time you startkeymaerax.jar
or usejava jar keymaerax.jar
from command line.  "[launcher] WARNING: A lock file exists but nothing is bound to the KeYmaera X web server's port.
Deleting the lock file and starting KeYmaera X. If you experience errors, try killing all
instances of KeYmaera X from your system's task manager."
Shut down other KeYmaera X instances. If no KeYmaera X is running delete~/.keymaerax/lockfile
orC:\Users\[You]\.keymaerax\lockfile
before restarting KeYmaera X.  If KeYmaera X acts weird after an update, clean your local cache by removing the directory
~/.keymaerax/cache
. You can also rename the model and proof database~/.keymaerax/keymaerax.sqlite
. It is good practice to periodically export KeYmaera X proof archives to separate files.  "Fatal error: cannot find the required native library named JLinkNativeLibrary." means that Mathematica is unavailable and the Z3 solver will be used instead. Install Mathematica or Wolfram Engine and specify its path, more details.
 "Exception in thread "main" java.lang.UnsupportedClassVersionError: ... has been
compiled by a more recent version of the Java Runtime (class file version X), this version of the Java Runtime only recognizes class file versions up to Y" indicates that you need to upgrade Java JDK to version 1.8+. You can check which version of Java you use by running:
java version
 The error
Invalid or corrupt jarfile
indicates that you need to upgrade Java JDK to version 1.8+. You can check which version of Java you use by running:java version
 "WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance." can be safely ignored.
 See More detail on potential 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 userdefined 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 soundnesscritical prover core.
Recent news: 06/17/2021: KeYmaera X 4.9.4 release
Provides an improved definitions UI to supply proof parameters and modeling assumptions, more robust tactic recording with formula search locators everywhere, tactic branch labels, as well as backend tool and parser updates. [UI] Tactic syntax highlighting, executing custom tactics from tactic editor with altclick (atomic) or shiftclick (stepbystep)
 [Tactic] positivemention
using
, e.g.QE using "x>0 :: x=0 :: nil"
hides all but the indicated formulas  [Tactic] formula search locators when recording tactics by clicking
 [Tactic] search locator notation #...# to identify subpositions, e.g.,
dI('R=="x>=0 > #[{x'=1}]x>=0#")
 [Tactic] branch labels and case matching,
e.g.,loop("J", 'R=="[{a;}*]S") ; <("Init": r, "Use": s, "Step": t)
to execute tacticr
on branch "Init" etc.
e.g.,andR('R=="x>=0 & y<=2") ; <("x>=0": s, "y<=2": t)
to execute tactics
on branch "x>=0" etc.  [Tactic] better support for differential symbols such as
x'
in quantifiers  [Tactic] improved ODE support for stability proofs [TACAS'21]
 [Backend] support for Mathematica 12.2 and 12.3 (MacOS)
 01/25/2021: KeYmaera X 4.9.3 release
Provides a substantially updated ModelPlex UI and core/parser updates. [ModelPlex] Web UI for ModelPlex process, artifacts, code export, and proofs
 [Core] Barcan axiom to commute quantifiers with program postconditions
 [Parser] vectorial taboos in systems/programs/functionals/predicationals
 [UI] Lemma UI bug fixes
 12/02/2020: KeYmaera X 4.9.2 release
Provides ODE liveness tactics, constructive differential game logic, a preview of a new proof language Kaisar, and UI improvements. [UI] ODE liveness tactics accessible from ODE menu
 [UI] Extended tactic menus: simplify, expand special function symbols, abbreviate terms, alpharename, extended tactics for hybrid programs and differential equations
 [UI] Tactic application from menu: position selection dialog, Alt/Option click in menu to apply tactics at the first applicable position without selection
 [UI] Live syntax checking in model upload dialog
 [Tactic] ODE liveness tactics: differential variant to prove ODE progress, ODE unification to combine evolution domain constraints, diamond ODE postcondition refinement, and diamond ODE evolution domain constraint refinement
 [Tactic] Improved usage of semantic renaming allows applying axioms and tactics despite the presence of program/game constants, e.g.
[x:=*;][a;]x>=0
turns into\forall x [a;]x>=0
 [Tactic] Alpharename bound occurrences of variables, e.g., knowing
x=y
, rename[{x'=x}]x>=0
to[{y'=y}]y>=0
 [Logic] Constructive differential game logic
 [Preview] New proof language Kaisar
 [Backend] Realarithmetic witnesses with sumofsquares solver, accessible from the tools menu
 11/02/2020: KeYmaera X 4.9.1 release
Better access to liveness tactics from the menu, improved differential ghosts, extended configuration options, and better support for nary predicates and function symbols in tactic arguments. [UI] Liveness tactics accessible from HP menu
 [UI] Expand predicate symbols with leftclick
 [UI] Advanced configuration in preferences
 [Tactic] Differential ghosts: support for additional input shapes, improved postcondition transformation considers evolution domain constraints, improved error messages
 [Backend] Z3 configurable local installation directory
 [Parser] Annotations bind strongest
 [Parser] Improved support for nary predicate and function symbols in tactic arguments
 [Tools] Code generator: flat conjunctions in quantitative monitors
 10/09/2020: KeYmaera X 4.9 major release
Restructured tactic framework and module separation. Model organization, shortcut notation in user definitions, improved support for starting and checking lemmas. [UI] More transparent display of proof rules with and without context
 [UI] Differential invariant (dI) proofs can be constructed interactively in the UI with
dIrule
. Automatic completion is available asdIclose
 [UI] Organize models into folders with hierarchical archive entry names
 [UI] Prove lemmas used in a theorem when opening the theorem, start new lemmas from open proof subgoals
 [Tactic] Framework restructuring, Scala annotation macros
@Axiom
for derived axiom registration,@Tactic
for tactic registration, tactic presentation, and tactic documentation  [Tactic] Stepbystep replay: expand definitions, use lemmas
 [Tactic] Framework extensions and robustness: polynomial arithmetic, differential equation proving, Taylor models, sumofsquares solving
 [Backend] Basic heuristic for timetriggered systems in Pegasus invariant generator
 [Backend] Update Z3 4.8.9
 [Parser] Shortcut notation for unary function symbols, system constants, unary predicates and predicationals; uniform across definitions, models, annotations, and tactics
 [Parser] ASCII game symbol for demonic choice '' synonymous with '∩'
 [Core] Compilable standalone to
keymaeraxcore.jar
 05/04/2020: KeYmaera X 4.8 major release
Restructured and reviewed microkernel and extended kernel. Extended differential equation invariant generation, and more flexible user definitions, significant performance improvements. [Core] Restructured and reviewed microkernel and extended kernel
 [Core] Designseparation between trusted external QE tools and additional nonsoundnesscritical external tools
 [Core] Semantic uniform renaming of rules
 [Core] Derived several axioms as lemmas
 [UI] Expand function, predicate, and program definitions on demand, introduce new definitions in the proof (e.g., abstract loop invariant predicate
J(x,y,z)
instead of concretex+y>=z
formula) and expand on demand later  [UI] Autologin for singleuser environments
 [Backend] Extended invariant generator Pegasus for differential equations (linear and nonlinear systems, improved generation strategy)
 [Backend] New native Java BigDecimal tool for variablefree exact arithmetic evaluation
 [Parser] Unicode game symbols for demonic choice '∩' and demonic repetition '×'
 [Performance] QE result caching
 [Performance] Faster parsing and printing of provables and lemmas
 [Performance] Faster lemma storage/retrieval from database
 [Performance] Runtime contracts disabled by default, can be enabled with
java ea
and disabled withjava da
 [Platform] Updated support for latest Java Virtual Machine and JDK versions
Older News and Older Versions
Archive of older news since the first public release 04/18/2015.