Download

KeY 2.12

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.

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 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.

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.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 java -jar key*-exe.jar.
Source and Binary ArtefactsThe classical KeY distribution containing a single jar file with all components, sources and JavaDoc files.

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 are 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'