
⇓ Download ⇓
or try Online 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. 
Startup Issues 
 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. JDK for x86 CPU architecture is strongly recommended for Mathematica compatibility, e.g., first install JDK 1.8 version 351 then update it).
 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 1013 for x64 CPU architecture but ARM Mathematica should work)
 Free alternative: Install Wolfram Engine version 12+ (for x64 CPU architecture but ARM Wolfram should work. Needs active internet and periodic manual license reactivation)
 Builtin: Z3 Solver (less functionality)
 Optional addon: Install and link both Mathematica and MatLab to improve KeYmaera X invariant generator Pegasus.
 Best functionality: Install Mathematica (version 1013 for x64 CPU architecture but ARM Mathematica should work)
 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 
 MacOS: Error
"keymaerax.jar" cannot be opened because it is from an unidentified developer
Workaround: in Finder use the Rightclick→Open menu the first time you startkeymaerax.jar
or usejava jar keymaerax.jar
from command line.  "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"
Workaround: 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."
Workaround: This warning can be safely ignored. 
"Fatal error: cannot find the required native library named JLinkNativeLibrary."
Workaround: Mathematica is unavailable and the Z3 solver will be used instead. Install Mathematica or Wolfram Engine and specify its path, more details.  Ubuntu:
Error: {PATH_TO_JVM}: symbol lookup error: {PATH_TO_JLINK}: undefined symbol: uuid_generate
Workaround: See instructions 
"[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."
Workaround: 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. 
Invalid or corrupt jarfile
Workaround: upgrade Java JDK to version 1.8+. You can check which version of Java you use by running:java version
 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: 20230606: KeYmaera X 5.0.2 release
 Command line options: Z3 path, KeYmaera X home directory
 Monitoring: support for interpreted symbols, improved Python exporter
 Definitions: predefined interpreted symbol
tan
 UI: animate finished proof (autoreplay)
 20221123: KeYmaera X 5.0.1 release
Provides bug fixes and a tactic to prepare quantifier elimination queries. Tactics: tactic
prepareQE
with heuristics for equality rewriting, introducing abbreviations, and forming the universal closure of a sequent  Tactics: tactic
rcf
to complete a query with an external tool  Tactics: tactic
qe
combinesprepareQE
andrcf
.
 Tactics: tactic
 20220811: KeYmaera X 5 major release
Provides a definition package for userdefined functions, major parser rewrite, keyboard shortcuts during proofs, tactic performance improvements, and tool improvements. Definitions: adds support for userdefined functions whose graphs can be implicitly characterized by dL formulas, such as the exponential and trigonometric functions, as solutions of differential equations. Properties of those userdefined functions can be proved using dL's differential equation reasoning principles. A highlevel interface for defining functions and nonsoundnesscritical tactics automate lowlevel reasoning over implicit characterizations in hybrid system proofs. Builtin definitions that can be used out of the box in models include
exp
,sin
,cos
,Pi
, andE
.  UI: keyboard shortcuts for common proof tasks (customizable through
.keymaerax/hotkeys.js
file in home directory)  Parser: complete parser reimplementation with support for userdefined functions, full tactic support in web UI parsing
 Tactics: performance improvement with builtin forward tactics replacing (some) interpreted tactics
 Tools: command line conversion tools from KeYmaera X format to SMTLib format (
convert kyx2smt
) and Wolfram format (convert kyx2mat
)  Tools: improved Z3based simplifier
 Definitions: adds support for userdefined functions whose graphs can be implicitly characterized by dL formulas, such as the exponential and trigonometric functions, as solutions of differential equations. Properties of those userdefined functions can be proved using dL's differential equation reasoning principles. A highlevel interface for defining functions and nonsoundnesscritical tactics automate lowlevel reasoning over implicit characterizations in hybrid system proofs. Builtin definitions that can be used out of the box in models include
 20220218: KeYmaera X 4.9.9 release
Provides UI bug fixes and some tactic performance improvements UI: display invariant generator (Pegasus) suggestions in
dC
differential cut dialog  Docker container: Matlab support
 Tactics: bug fixes for definition expansion
 Tactics: faster forward implementation of several frequently used tactics
 Security patch: Log4j 2.17.1 (addresses CVE202145105, CVE202145046, CVE202144832, CVE202144228)
 UI: display invariant generator (Pegasus) suggestions in
 20211124: KeYmaera X 4.9.8 release
Provides a security patch and tactic implementation updates. Tactic: forwardstyle implementation of unification calculus tactics
 Security patch: Log4j 2.15.0 (addresses CVE202144228)
 20211124: KeYmaera X 4.9.7 release
Provides support for switched systems, a fixpoint tactic for hybrid games, as well as UI and robustness improvements. Switched systems: hybrid automaton modeler: Models→Templates→Switched Systems
 Tactic: new stability and attractivity tactics for switched systems
 Tactic: new fixpoint tactic
fp
for hybrid games and hybrid systems  UI: tactic and model editor bug fixes
 UI: browse all tactics
 Code generator: export definitions
 Core: Use fixpoint rule FP instead of the interderivable induction rule ind to save proof effort.
 20211006: KeYmaera X 4.9.6 release
Provides UI and robustness improvements. UI: tactic editor improvements, run tactics from editor directly
 UI: save models while editing
 Code: Export ModelPlex to Python
 Tactic: support for uninterpreted function symbols of arity>0 in QE
 Parser: improved error messages for program constants
 20210902: KeYmaera X 4.9.5 release
Provides improved interaction between tactics editing and sequent view. UI: selected tab gets highlighted in tactic editor, cursor position switches tabs
 UI: proof state displayed below tactic editor according to cursor position
 UI: formula icons ("eye") to configure positivemention "using" by mouse
 UI: fast manual QE/CEX exploration with temporary formula hiding ("eye")
 Tactics: differential cut for constant quantities, e.g.,
dC("x^2+y^2=const()", 1)
 Docker container with KeYmaera X server
 20210617: 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)
 20210125: 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
 20201202: 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
 20201102: 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

20201009: 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

20200504: 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.