Source or read
Book or watch
InstallationKeYmaera X should run out-of-the-box after you install it:
- Install Java JDK 1.8 (recommended version 1.8 but versions 1.9-1.10 are possible yet 1.11 is not)
- Download KeYmaera X
- Run KeYmaera X either by clicking on the
or by starting it from command line:
java -jar keymaerax.jar
- Log in to your KeYmaera X User Interface that will open in your web browser:
- The KeYmaera X User Interface will show you different options for arithmetic:
- Start exploring KeYmaera X or read quick user guide
KeYmaera X is available as open source under GPLv2. If you prefer to use KeYmaera X under another license, just contact Carnegie Mellon University's Center for Technology Transfer and Enterprise Creation.
- On macOS, the error
"keymaerax.jar" can't be opened because it is from an unidentified developerindicates that you have to use the Right-click→Open menu the first time you start
- The error
Invalid or corrupt jarfileindicates that you need to upgrade Java JDK to version 1.8. You can check which version of Java you use by running
- The error
java.lang.module.FindException: Module java.xml.bind not foundindicates that you need to downgrade Java JDK to version 1.8 till 1.10, because JDK 1.11 is not compatible with Scala yet.
- Errors related to
JLinkNativeLibraryare caused by incompatibilities such as Java JDK 1.8 in combination with Mathematica 9. It is recommended to use Mathematica 10+. Or they may be caused by operating system configuration or bit-width issues.
- If KeYmaera X acts weird after an update, clean your local cache by removing the directory
~/.keymaerax/cache. You can also rename the model and proof database
~/.keymaerax/keymaerax.sqlite. It is good practice to periodically export KeYmaera X proof archives to separate files.
NewsKeYmaera 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, user-defined tactics easily definable custom proof search procedures, and more sophisticated ODE invariant generation. KeYmaera X also comes with a significantly more versatile user interface. Above all, KeYmaera X has a substantially smaller soundness-critical prover core.
- 10/10/2019: Best Tool Paper Award at FM 2019 for Pegasus, the continuous invariant generator for KeYmaera X
- 10/04/2019: KeYmaera X 4.7.3 release
new Wolfram Engine backend and proof inspection features.
- [Backend] Wolfram Engine backend supporting real arithmetic and ODE invariant generation
- [UI] Expand tactic step details by clicking (≡)
- [UI] Reuse finished proofs as lemmas (Browse→Lemmas menu)
- [Tactics] Explore a model using loop and ODE invariant annotations and show all failing branches (Explore button)
- [Tactics] Proof state labeling: edit branch tab names to set labels in the proof
- 09/10/2019: KeYmaera X 4.7.2 release
UI and backend stability updates.
- [Backend] Stability fixes
- [Parser] Support for model illustration links
- [UI] Model illustration images
- 09/01/2019: KeYmaera X 4.7.1 release
User interface improvements and tactic syntax updates.
- [UI] New tool: Pegasus invariant generator
- [UI] Additional help and examples, improved undo, improved formula pretty printing/layout
- [Tactics] Syntax update double quotation marks "..." for tactic arguments
- [Tactics] Partial QE with simplification using assumptions
- [Tactics] ODE automation improvement (counterexamples, condition search)
- 06/16/2019: KeYmaera X 4.7.0 release
major update, automation improvement, performance, and stability updates
- [Core] Fast one-pass uniform substitution
- [Backend] Invariant generator Pegasus for differential equations (Qualitative Analysis, First Integrals, Darboux Polynomials, Barrier Certificates)
- [Backend] Z3 update 4.8.4
- [Parser] Significant performance improvement
- [Tactics] Improved ODE automation
- [Tactics] Interval arithmetic: proves quantifier-free real arithmetic when the antecedent has numerical bounds for all free variables of the succedent
- [UI] Command line: -prove -verbose for tactic progress printing
- [Code Synthesis] Monitor C code generator: IDs now identify failed monitor sub-condition