KeY 2.12 is the latest stable release and has been published on August 18th, 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.
Download or Start
KeY requires Java version 11 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.0-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 not yet updated to KeY 2.10.0. The linked versions are still based on KeY 2.6.3.
|Update Site Name:||KeY Eclipse Extensions|
|Update Site URL:||https://formal.iti.kit.edu/key/download/releases/2.6/eclipse/|
Unstable Development Versions (Nightly Builds)
You can download a current snapshot of the KeY development version below.
|Just download and start via |
|Source and Binary Artefacts||The classical KeY distribution containing a single jar file with all components, sources and JavaDoc files.|
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:
An overview of the artifacts are given here: https://central.sonatype.com/namespace/org.key-project.
Normally, you need the artifact
key.ui if you want to use KeY as a library.
Other artifacts are also exported, and are included transitively if required.
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:
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: