
Download
or try Online or read Book or list Documents 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/
 Strongly 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
KeYmaera X is available as open source under GPLv2. If you would rather use KeYmaera X under another license, just contact Carnegie Mellon University's Center for Technology Transfer and Enterprise Creation.
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. 11/26/2018: KeYmaera X 4.6.2 release
Performance and robustness improvements  11/26/2018: [Tactics] ODE solver performance improvements
 11/26/2018: [Tactics] Tactic positioning and input robustness, including quantifier instantiations, abbreviations and special functions, input flexibility for differential ghosts, monotonicity
 11/26/2018: [Parser] Improved error messages
 11/26/2018: [UI] Robustness improvements, backend tool status polling, polling performance improvement
 10/09/2018: KeYmaera X 4.6.1 release
Stability release  10/09/2018: [Parser] Improved stability and error reporting
 10/09/2018: [Tactics] Preview: modular componentbased proofs
 09/22/2018: KeYmaera X 4.6.0 release
Major improvement in KeYmaera X file format and parser, general tool stability and automation  09/22/2018: [Tools] Automated proof backup in plaintext archive files
 09/22/2018: [Tools] Improved tool stability, tool busy indicator, and tool restart and connection testing
 09/22/2018: [Tactics] Improved automation on typical model shapes, ODE tactic improvements
 09/22/2018: [Parser] Major update to archive syntax and parser error reporting:
ArchiveEntry "Example" Description "Illustrates the main archive syntax changes". Definitions /* function symbols cannot change their value */ Real A = 5; /* realvalued acceleration constant defined as 5 */ Real B; /* realvalued braking constant is uninterpreted */ Bool inv(Real v) <> v>=0; /* invariant formula definition */ End. ProgramVariables /* program variables may change their value over time */ Real x, v; /* realvalued position and velocity */ Real a; /* current acceleration chosen by controller */ End. Problem A>0 & B>0 & v>=0 > [ { { ?v<=5; a:=A; ++ a:=0; ++ a:=B } { x'=v, v'=a & v>=0 } }* @invariant(inv(v)) ] v>=0 End. End.
 07/09/2018: KeYmaera X 4.5.0 release
Major improvements on automation, invariant generation, and differential equation automation.  07/09/2018: [New] Pegasus invariant generator for differential equations
 07/09/2018: [New] ODE automation tactics for axiomatic proofs from differential ghost and differential refinement axioms, proofs of barrier certificates, and proofs of invariance properties that involve Darboux polynomials
 07/09/2018: [Preview] Invariant generation for loops based on fixpointsearch over invariants for differential equations
 07/09/2018: [Tactics] Liveness: loop convergence with userdefinable convergence variable, improved <:=> assignment tactics
 07/09/2018: [Tactics] Extended proof search automation in the context of universal/existential quantifiers
 07/09/2018: [Tools] C code generator for structured monitors with subroutines and error message printing
 04/18/2018: KeYmaera X 4.4.3 release 3rd birthday release of KeYmaera X
 04/18/2018: [New] Tactic
barrier
proves barrier certificates of ODEs (automatically used inODE
tactic)
For example, provex>=0  [{x'=100*x^4+y*x^3x^2+x+c, c'=x+y+z & c>x}]x>=0
with tacticbarrier(1)
or tacticODE(1)
 04/18/2018: [New] Tactic
dbx
proves ODEs using Darboux polynomials (automatically used inODE
tactic)
For example, provex+z<0  [{x'=x^2, z'=z*x+y & y=x^2}]x+z<0
with tacticdbx({x},1)
or tacticODE(1)
 04/18/2018: [New] Model documentation and proof hints with
@invariant
annotations for ODEs
For example, provide a list of two differential invariants:[{x'=2,y'=1} @invariant(x>=old(x), y<=old(y))]p()
 04/18/2018: [New] Conditional differential invariant annotations
For example, provide a list of two differential invariants, one for each branch:[{a:=2; ++ a:=1;} ; {x'=a} @invariant( (x'=2 > x>=old(x)), (x'=1 > x<=old(x))) ]p()
 04/18/2018: [UI] Significant performance improvements
 04/18/2018: [Tactics] Tactic
dW
now keeps all initial conditions  04/18/2018: [Tactics] Configurable timeouts for tactics
QE
andODE
(configuration filekeymaerax.conf
)  04/18/2018: [Tactics] Combinator
s > t
runs tactics
first and then tactict
regardless of the result ofs
 02/28/2018: KeYmaera X 4.4.2 release
 02/28/2018: [Performance] Significant performance improvements by disabling logging by default
 02/28/2018: [UI] New web UI axiom and proof step browser
 02/28/2018: [UI] Hint display and tactic popover fixes
 02/28/2018: [Tactics] New loop induction with abstraction
throughout(inv,pos)
proves loopinit > [{a;b}*]safe
with throughout invariantinv
from subgoals: base case:
init > inv
 use case:
inv > safe
 induction steps:
inv > [a]inv
andinv > [b]inv
 base case:
 01/18/2018: KeYmaera X 4.4.1 release
 01/18/2018: Backend tool and tactic stability improvements
 01/18/2018: [New] Store and use lemma entries in
.kyx
archives:
Lemma "My lemma". ... End.
to store the given lemma under the identified name "My lemma". 
useLemma({`My lemma`},{`prop`})
to close goal by lemma, use propositional reasoning to adapt shape 
useLemmaAt({`My lemma`},{`1`},2)
to match lemma expression at subposition 1 with formula at sequent position 2

 01/18/2018: [New] Convert KeYmaera X proof terms to Isabelle dL proof checker
 01/18/2018: [New] Configuration is now stored in a text file
~/.keymaerax/keymaerax.conf
 01/18/2018: [New] Transform hybrid programs to C control code
 09/18/2017: 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: KeYmaera X 4.3.16 release
 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: KeYmaera X 4.3.15 release
 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: KeYmaera X 4.3.14 release
 07/28/2017: Fix: ODE solver tactic printing for
solveEnd
solution tactic with evolution domain constraint only at endpoint  07/27/2017: KeYmaera X 4.3.13 release
 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: KeYmaera X 4.3.12 release
 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: KeYmaera X 4.3.11 release
 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: KeYmaera X 4.3.10 release
 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: KeYmaera X 4.3.9 release
 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: KeYmaera X 4.3.8 release
 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: KeYmaera X 4.3.7 release
 03/20/2017: Parser supports ifthenelse statement
if (v^2>5) {a:=b;} else {a:=2;}
 03/09/2017: KeYmaera X 4.3.6 release
 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: KeYmaera X 4.3.5 release
 02/20/2017: UI bugfixes and stability improvements
 02/15/2017: KeYmaera X 4.3.4 release
 02/15/2017: Minor stability release generalizing the flexibility of the Axiomatic ODE Solver tactic
 02/13/2017: KeYmaera X 4.3.3 release
 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: KeYmaera X 4.3.2 release
 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: KeYmaera X 4.3.1 release
 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: KeYmaera X 4.3 release
 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: KeYmaera X 4.2.2 release
 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: KeYmaera X 4.2.1 release
 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: 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: KeYmaera X 4.2b2 release
 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: KeYmaera X 4.2b1 release
 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: KeYmaera X 4.1b4 release
 02/19/2016: UI bug fixes
 02/19/2016: KeYmaera X 4.1b3 release
 02/19/2016: UI improvements and bug fixes
 02/19/2016: Improved differential equation solving tactics
 01/22/2016: KeYmaera X 4.1b2 release
 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: KeYmaera X 4.1b1 release
 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: KeYmaera X 4.0b1 release
 09/25/2015: First public release of KeYmaera X source code, open source license GPLv2
 04/18/2015: First public KeYmaera X 4.0a1 release