KeY 2.12
KeY 2.12.2 is the latest stable release and has been published on November 10th, 2023. Some of the highlights are support for floating points, support for JML assert/assume statements, support for JML math modifiers (spec_bigint_math, spec_java_math, …), the proof slicing extension to minimize your proofs, and much more.
In case of questions about KeY, please start a discussion on GitHub or contact support@key-project.org.
Download or Start
KeY requires Java version 17 or newer and is tested on Linux, OS X and Microsoft Windows. The latest release can be found on GitHub under https://github.com/KeYProject/key/releases/latest. KeY can be started via java -jar key-2.12.2-exe.jar or via a simple double-click on the jar file. The accompanying CLI tools (“removegenerics” and “proofmanagement”) can be run with the same command, for details about the parameters see the Readme files in the repository.
Supported Java and JML Features
Previous KeY versions
The previous stable releases are KeY 2.10.0 and KeY 2.8.0. The versions KeY 2.6.x accompany the second KeY Book. You can find the KeY 2.6.x versions here. The last KeY 1.6 release is KeY 1.6.5 (released on April 18, 2013) and only provided for legacy reasons.
KeY-Based Eclipse Projects
The Eclipse based projects are still based on KeY 2.6.3.
Detailed information about the provided Eclipse extensions can be found here. To install KeY 2.6.3 for Eclipse 4.7 Oxygen (other 4.x versions (Luna/Mars/Neon) should work as well).
| Update Site Name: | KeY Eclipse Extensions |
| Update Site URL: | https://formal.kastel.kit.edu/~key/download/releases/2.6/eclipse/ |
Unstable Development Versions (Nightly Builds)
You can download a current nightly release of KeY from GitHub under https://github.com/KeYProject/key/releases/tag/nightly. The artifacts available are:
Just download and start via java -jar key*-exe.jar. | |
| Sources | A single zip file with all components and sources of KeY. |
Maven Repository
If you intend to use KeY as a (Java) library and want to access its API, you can include KeY as a dependency in Maven, gradle, sbt (or similar managers). Since 2.12.0, KeY is present on Maven Central. You’ll find us under the group id: org.key-project.
An overview of the artifacts is given here: https://central.sonatype.com/namespace/org.key-project.
Normally, you need the artifact key.core or key.ui if you want to use KeY as a library.
Other artifacts are also exported, and are included transitively if required.
Example Project
You can find an example project on how to use KeY with Gradle here: https://github.com/KeYProject/key-java-example
Using the Public Repository
Beside of the zipped distribution, you have access to the Git repository at Github. The mirror contains the stable (tested and validated master) and release branches of KeY. You can find the repository here:
https://github.com/keyproject/key
Using the public repository is the best choice if you use (a) gradle for building your project and (b) you plan to make changes to KeY. Then you should add KeY as a submodule to your project:
$ git submodule add https://github.com/keyproject/key
And add to your settings.gradle:
includeBuild 'key/key'