|
⇓ 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 out-of-the-box 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)
- Built-in: Z3 Solver (less functionality)
- Optional add-on: 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 out-of-the-box 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 Right-click→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 user-defined 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 soundness-critical prover core.
Recent news:- 2024-06-26: 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
- 2023-06-06: 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 (auto-replay)
- 2022-11-23: 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
- 2022-08-11: KeYmaera X 5 major release
Provides a definition package for user-defined functions, major parser rewrite, keyboard shortcuts during proofs, tactic performance improvements, and tool improvements.- Definitions: adds support for user-defined 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 user-defined functions can be proved using dL's differential equation reasoning principles. A high-level interface for defining functions and non-soundness-critical tactics automate low-level 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 re-implementation with support for user-defined 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 SMT-Lib format (
-convert kyx2smt
) and Wolfram format (-convert kyx2mat
) - Tools: improved Z3-based simplifier
- Definitions: adds support for user-defined 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 user-defined functions can be proved using dL's differential equation reasoning principles. A high-level interface for defining functions and non-soundness-critical tactics automate low-level reasoning over implicit characterizations in hybrid system proofs. Builtin definitions that can be used out of the box in models include
- 2022-02-18: 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 CVE-2021-45105, CVE-2021-45046, CVE-2021-44832, CVE-2021-44228)
- UI: display invariant generator (Pegasus) suggestions in
- 2021-11-24: KeYmaera X 4.9.8 release
Provides a security patch and tactic implementation updates.- Tactic: forward-style implementation of unification calculus tactics
- Security patch: Log4j 2.15.0 (addresses CVE-2021-44228)
- 2021-11-24: 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.
- 2021-10-06: 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
- 2021-09-02: 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 positive-mention "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
- 2021-06-17: 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 alt-click (atomic) or shift-click (step-by-step)
- Tactic: positive-mention
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 sub-positions, 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)
- 2021-01-25: 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
- 2020-12-02: 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, alpha-rename, 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: Alpha-rename 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: Real-arithmetic witnesses with sum-of-squares solver, accessible from the tools menu
- 2020-11-02: KeYmaera X 4.9.1 release
Better access to liveness tactics from the menu, improved differential ghosts, extended configuration options, and better support for n-ary predicates and function symbols in tactic arguments.- UI: Liveness tactics accessible from HP menu
- UI: Expand predicate symbols with left-click
- UI: Advanced configuration in preferences
- Tactic: Differential ghosts: support for additional input shapes, improved post-condition transformation considers evolution domain constraints, improved error messages
- Backend: Z3 configurable local installation directory
- Parser: Annotations bind strongest
- Parser: Improved support for n-ary predicate and function symbols in tactic arguments
- Tools: Code generator: flat conjunctions in quantitative monitors
-
2020-10-09: 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: Step-by-step replay: expand definitions, use lemmas
- Tactic: Framework extensions and robustness: polynomial arithmetic, differential equation proving, Taylor models, sum-of-squares solving
- Backend: Basic heuristic for time-triggered 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
keymaerax-core.jar
-
2020-05-04: 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: Design-separation between trusted external QE tools and additional non-soundness-critical 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: Auto-login for single-user environments
- Backend: Extended invariant generator Pegasus for differential equations (linear and non-linear systems, improved generation strategy)
- Backend: New native Java BigDecimal tool for variable-free 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.