Install KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

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.

             

1. Install Java 11+ (tested till Java 22).
2. Download KeYmaera X
3. 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

4. Log in to your KeYmaera X User Interface that will open in your web browser:
   

     http://localhost:8090/

5. The KeYmaera X User Interface will show you different options for arithmetic that you can configure in the KeYmaera X→Preferences menu:
   1. Best functionality: Install Mathematica (version 10+ for x64 CPU architecture or ARM64 CPU architecture)
      
   2. Free alternative: Install Wolfram Engine version 12+ (for x64 CPU architecture or ARM64 CPU architecture. Needs active internet and periodic manual license reactivation)
      
   3. Built-in: Z3 Solver (less functionality)
   4. Optional add-on: Install and link both Mathematica and MatLab to improve KeYmaera X invariant generator Pegasus.
   Only unusual use cases need advanced configuration in the menu KeYmaera X→Preferences→Advanced.
6. Start exploring KeYmaera X or read user guide.

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 start keymaerax.jar or use java -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.

• New KeYmaera X Tutorial
• List All releases of KeYmaera X

• 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 combines prepareQE and rcf.
• 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, and E.
  • 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
• 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)
• 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 tactic r on branch "Init" etc.
    e.g., andR('R=="x>=0 & y<=2") ; <("x>=0": s, "y<=2": t) to execute tactic s 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 as dIclose
  • 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 concrete x+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 with java -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.

Archive of older releases of KeYmaera X since 2015.