
Download
or try Online or consult API Doc or study Source 
Download
KeYmaera X should run outofthebox after you download KeYmaera X. If you are having difficulties, there is also publicly hosted demo. Install Java JDK (version 1.8+ recommended)
 Download KeYmaera X
 Run KeYmaera X either by clicking on the
keymaerax.jar
file
or by starting it from command line:java jar keymaerax.jar
 The KeYmaera X User Interface will open in your web browser at:
http://localhost:8090/
 Recommended: Install Mathematica (recommended version 10+)
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
News
KeYmaera X is a stable release surpassing almost all capabilities of its predecessor KeYmaera 3. KeYmaera X provides numerous features that KeYmaera 3 users have been dreaming of for a long time. For example, userdefined tactics and easily definable custom proof search procedures. KeYmaera X also comes with a versatile user interface. 09/18/2017: Release of KeYmaera X 4.4 major release
 09/18/2017: Core: Uniform substitutions for Nary formula and function definitions.
 09/18/2017: Parser: Use
._i
to refer to the ith argument. For example, define a binary function
sum
as:sum(R,R) = ( ._0 + ._1 ).
 define predicate
sumgt
as:sumgt(R,R,R) <> ( sum(._0,._1) > ._2 ).
 define a hybrid program
increment
as:HP increment ::= { x:=x+1; }.
 define a binary function
 09/18/2017: Tactics: New: use finished proofs as lemmas.

useLemma({Name of proved model})
when the open goal matches the lemma literally. 
useLemma({Name of proved model}, {prop})
to apply the lemma with propositional reasoning to make goals match.

 09/18/2017: Tools: New: proof statistics after checking proof archives with
check
command line argument.  09/18/2017: Tools: New: C control code synthesis (feature preview)
 09/18/2017: Tools: Improved: C monitor code synthesis (feature preview)
 09/18/2017: Stability improvements: archive checking, ODE solution ordering
 08/26/2017: Release of KeYmaera X 4.3.16
 08/26/2017: Three new tactics for automatic nth Taylor approximation:

circularApproximate(s,c,n,pos)
: for circular dynamics{s'=c, c'=s}

expApproximate(e,n,pos)
: for exponential dynamics{e'=e}

autoApproximate(n,pos)
: Tries to find{e'=e}
then tries to find{s'=c,c'=s}
and applies the relevant approximation tactic.

 08/26/2017: More powerful formula editing in UI:

expand(expr)
will expand functions min/max/abs, e.g.,expand(abs(0)) >= 0

abbrv(term,name)
will abbreviate terms, e.g.,x+abbrv(2+3,five) >= 0

 08/26/2017: Search and apply lemmas
 Autocompletion search box in the rule application dialog
 Click lemma subformulas to adjust the direction in which lemmas are applied
 08/26/2017: User interface startup improved. Browser no longer opens automatically on Linux, because this made Java hang on some configurations.
 08/26/2017: Various improvements to the tactics framework and standard library.
 08/26/2017: Bug fix in how numbers are prettyprinted.
 08/08/2017: Release of KeYmaera X 4.3.15
 08/08/2017: UI: Improvements to presentation and browse mode
 08/08/2017: UI: Render nullary function symbols
b()
without parentheses asb
 08/08/2017: Updates Z3 solver to 4.5.0, with improved QE support for machines without Mathematica.
 08/08/2017: Improved update code for Windows.
 07/28/2017: Release of KeYmaera X 4.3.14
 07/28/2017: Fix: ODE solver tactic printing for
solveEnd
solution tactic with evolution domain constraint only at endpoint  07/27/2017: Release of KeYmaera X 4.3.13
 07/27/2017: Proof browsing display proof step justification
 07/27/2017: New: Model editing
 07/27/2017: Web UI and backend fixes and improvements
 07/27/2017: Feature preview: exercise models with placeholders
__________
 07/20/2017: Release of KeYmaera X 4.3.12
 07/20/2017: New: stepbystep proof browsing to illustrate and explain proofs
 07/20/2017: New: tactic tooltips on proof step in sequent proofs
 07/20/2017: Revamped proof step highlighting
 07/20/2017: User interface and backend stability improvements
 07/11/2017: Release of KeYmaera X 4.3.11
 07/11/2017: Substantially improved Web UI performance by significant factors.
 07/11/2017: New: Builtin text editor to edit new models from Models>New Model>Edit.
 07/11/2017: New: Models can be plain differential dynamic logic formulas without variable declarations such as
x>=0 & a>0 > [{x'=v,v'=a & v>=0}] x>=0
 07/11/2017: New: Abbreviate terms when editing formulas with special function symbol
abbrv(term)
orabbrv(term, abbreviation)
For examplex+abbrv(3+2, v) > y
becomesx+v > y, v = 3+2
with all occurrences of3+2
replaced byv
.  07/11/2017: Improved differential cut tactic: refer to initial values of arbitrary terms with
old(term)
and support for multiple uses ofold(term)
 07/11/2017: Improved syntax for differential ghost tactic:
dG({`y'=a*y+b`}, {`G`}, 1)
instead ofdG({`y`},{`a`},{`b`}, {`G`}, 1)
 07/11/2017: Beta: Parse unicode syntax such as ∧ ∨ ∀ ∃ → ≥
 07/11/2017: New: browse model archives on
web.keymaeraX.org/show/itp17/parachute.kya
or on localhost aslocalhost:8090/show/http://url/of/my.kya
 05/24/2017: Release of KeYmaera X 4.3.10
 05/24/2017: ODE solver generalized for diamond ODEs
 05/24/2017: UI syntax highlighting and interaction improvements
 05/24/2017: UI displays proof hints on how to proceed
 05/24/2017: UI displays equality rewriting in context menu
 05/24/2017: Workaround for recent Mathematica bugs by using a TCP version of J/Link
 05/24/2017: Bugfix model import
 04/27/2017: Release of KeYmaera X 4.3.9
 04/27/2017: Tactic input validation to prevent impossible proof attempts
 04/27/2017: Performance improvements in user interface
 04/27/2017: Function and predicate definitions in
.kyx
modelsFunctions. R init() = (10). /* fixed initial position */ R obs(). /* arbitrary obstacle position */ R dist(R) = ((.)obs()). /* distance of argument (.) to obstacle */ B safe(R) <> (dist((.))>5). /* safe distance of arg (.) from obstacle */ End. ProgramVariables. R x. /* position */ R v. /* velocity */ End. Problem. x=init() & safe(init()) & v>0 > [{x'=v}] safe(x) End.
 04/18/2017: Release of KeYmaera X 4.3.8
 04/18/2017: Substantial performance improvements
 04/18/2017: Improved support for hybrid game proofs
 04/18/2017: Updated database format for performance
 03/20/2017: Release of KeYmaera X 4.3.7
 03/20/2017: Parser supports ifthenelse statement
if (v^2>5) {a:=b;} else {a:=2;}
 03/09/2017: Release of KeYmaera X 4.3.6
 03/09/2017: Stability improvements, including generalizations for differential equation solving
 03/09/2017: Concrete syntax updated to help disambiguate
Braces are now required around differential equations{x'=x^2,y'=2*x+y}
Constant symbolsc()
can now be used without parentheses in.kyx
problem files  02/20/2017: Release of KeYmaera X 4.3.5
 02/20/2017: UI bugfixes and stability improvements
 02/15/2017: Release of KeYmaera X 4.3.4
 02/15/2017: Minor stability release generalizing the flexibility of the Axiomatic ODE Solver tactic
 02/13/2017: Release of KeYmaera X 4.3.3
 02/13/2017: Edit: formula editing can rewrite formulas everywhere
 02/13/2017: Step into failed tactics to observe partial progress and debug the proof
 02/13/2017: ODE solver generalized to systems written in any order
 02/13/2017: Simplifier improvements
 02/13/2017: Stability advances
 01/28/2017: Release of KeYmaera X 4.3.2
 01/28/2017: New Learner's mode
 01/28/2017: Simplify differential equation tactics
 01/28/2017: UI stability and help improvements
 01/28/2017: Preview: Obtain internal details on tactical proof steps
 01/20/2017: Release of KeYmaera X 4.3.1
 01/20/2017: Get quick usage help with ? menu button on each page
 01/20/2017: Import and export for model/proof archive (
.kya
file).  01/20/2017: Synthesize verified safety metrics from ModelPlex
 01/20/2017: Improved automation of
ode
tactic for differential equations.  01/11/2017: Prover core fixes
 11/08/2016: Release of KeYmaera X 4.3
 11/08/2016: Add support for Differential Game Logic (dGL) for Hybrid Games
 11/08/2016: ModelPlex web UI integration for both controller and model monitors
 11/08/2016: Axiomatic ODE solver improvements (box and diamond properties as well as inplace solving)
 11/08/2016: UI improvements and bug fixes (tactic difference, tactic parser errors)
 11/08/2016: Stability improvements (unifier, UI, quantifier instantiation)
 09/28/2016: Release of KeYmaera X 4.2.2
 09/28/2016: Extraction and execution of tactics with input
 09/28/2016: Web user interface improvements
 09/28/2016: Tactic and lemma download on finished proof
 09/17/2016: Release of KeYmaera X 4.2.1
 09/17/2016: Significant performance advances for a snappier interaction with KeYmaera X
 09/17/2016: Readability improvements in tactic extraction
 09/17/2016: User interface polishing, improvements, and styling, including position highlighting
 09/17/2016: Faster database interaction
 09/17/2016: Prover core fixes for bound renaming (unexploited)
 09/17/2016: Inverse characteristic method for differential invariant generation
 09/17/2016: Better command line interfaces
 09/02/2016: Release of KeYmaera X 4.2 first stable release
 09/02/2016: User interface advances
 09/02/2016: Tactic extraction, tactic programming, and replay
 09/02/2016: Major backend tool improvements
 09/02/2016: KeYmaera X runs standalone without the need to install additional tools since it ships with the Z3 solver. Mathematica is recommended as an addon installation for advanced automation and simulation features, though.
 09/02/2016: Axiomatic differential equation solver with solvebyproof technology
 09/02/2016:
ODE
tactic for automatic proofs of differential equations  09/02/2016: Invariant and differential invariant generation techniques
 09/02/2016: Tutorial import feature
 09/02/2016: Faster unificationbased tactics
 09/02/2016: Significant prover core advances, fixes, and simplifications
 07/20/2016: Release of KeYmaera X 4.2b2
 07/20/2016: Axiomatic ODE Solver
 07/20/2016: Differential ghosts are now exposed in web UI (diffGhost)
 07/20/2016: Rewrite of the Mathematica interface for improved stability
 07/20/2016: Improved kernel functionality for interpreted functions
 07/20/2016: SSL mode for hosted web servers
 04/11/2016: Release of KeYmaera X 4.2b1
 04/11/2016: Major improvements to prover core
 04/11/2016: Pencil tool for simplifying arithmetic in place
 04/11/2016: Simple system simulation feature
 04/11/2016: Various bug fixes
 04/11/2016: Ships with tutorial examples from CPSWEEEK 2016
 03/01/2016: Release of KeYmaera X 4.1b4
 02/19/2016: UI bug fixes
 02/19/2016: Release of KeYmaera X 4.1b3
 02/19/2016: UI improvements and bug fixes
 02/19/2016: Improved differential equation solving tactics
 01/22/2016: Release of KeYmaera X 4.1b2
 01/22/2016: Draganddrop support for constructing proofs
 01/22/2016: Major performance enhancement make KeYmaera X snappier to use
 01/22/2016: More userfriendly error messages when things go wrong
 01/15/2016: First public release of KeYmaera X 4.1b1
 01/15/2016: Entirely new user interface with native sequent proofs
 01/15/2016: Support proofbypointing intuition in user interface
 01/15/2016: Contextual proof development supported in user interface
 01/15/2016: New Bellerophon tactic language and tactic framework
 01/15/2016: Undo proof steps, stopping tactics, counterexample support
 01/15/2016: Proof storage format and proof management backend redesigned
 09/25/2015: First public release of KeYmaera X 4.0b1
 09/25/2015: First public release of KeYmaera X source code, open source license GPLv2
 04/18/2015: First public release of KeYmaera X 4.0a1