
⇓ Download ⇓
or get Source and read Book and watch Videos and follow Tutorial 
Quickly
Installation
The KeYmaera X aXiomatic Tactical Theorem Prover for Hybrid Systems should run outofthebox on macOS or Linux or Windows after you install it.
 Install Java 11+ (tested till Java 22).
 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 the KeYmaera X→Preferences menu:
 Best functionality: Install Mathematica (version 10+ for x64 CPU architecture or ARM64 CPU architecture)
 Free alternative: Install Wolfram Engine version 12+ (for x64 CPU architecture or ARM64 CPU architecture. 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 10+ for x64 CPU architecture or ARM64 CPU architecture)
 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 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.  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: 20240626: KeYmaera X 5.1.0 release
 Increased minimum supported Java version to JDK 11 (tested up to JDK 22)
 Improved automatic Mathematica path detection
 Fixed bug preventing KeYmaera X from running on Windows
 Fixed axiom derivation issues on startup
 Fixed incorrect syntax errors in webui text editor
 Removed
security
CLI flag and webui SSL support
 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.