KeY 2

KeY 2.8 is the latest stable release and has been published on December 18th, 2020. It comes with an overhauled user interface and many new features.

In case of questions about KeY please contact:

Previous KeY versions

We provide still some previous versions:
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 Hoare has its own dedicated download page.

Download or Start

KeY requires Java version 8 or newer and is tested on Linux, OS X and Microsoft Windows.

  • Single Click Jar: KeY-2.8.0.jar (officially supported install version)
    • Download and start via java -jar key-2.8.0-exe.jar
      or via a simple double click on the jar file
  • Binary Version:
  • Source Code:

Supported Java and JML Features

New Features in 2.8

  • Support for bounded sums
  • Innovative and improved treatment of loops via loop contracts and a new loop invariant rule based on loop scopes
  • Proof bundles: Saving proofs incl. resources into one zip file
  • Source code view with highlight for symbolically executed statements
  • Origin Labels: Track the origin of the formulas (e.g. if they stem from a precondition, postcondition or loop invariant)
  • Heatmaps (know which formulas have been modified recently)
  • Interaction Logging
  • Flexible and configurable layout, Improved search, proof exploration, etc. 
  • New proof script command
  • Full changelog

KeY-Based Eclipse Projects

The Eclipse based projects are not yet updated to KeY 2.8.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:

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 Artefacts The 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). We provide a Maven repository that contains the artifcats for the KeY packages mentioned below. The repository contains the current official release and is irregularly updated with the stable nightly-build version.

The Maven repository is hosted at our Gitlab instance. For using KeY you should include key.core or key.ui into your build script.

Group Idorg.key_project
Artifacts Idkey.core
Version:2.8.0 (current release)
2.6.3 (old release)
2.9.0-SNAPSHOT (weekly-published nightly build)

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:

Use with Maven


Use with Gradle

repositories { 
  maven { 
    url  ""    

Using the Public Repository

Beside of the zipped distribution you have access to a mirror of the internal Git repository. 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

And add to your settings.gradle:

includeBuild 'key/key'

Known Problems & Workarounds

Strings “don’t work” in projects with auto-generated stubs

Problem descriptionReasonWorkaround
When using the (otherwise very practical!) feature of the KeY eclipse plugin which automatically generates stubs (empty methods with default specifications) for included library methods, it might happen that symbolic execution of Java programs gets stuck at a place like str = "foo";, where str is a variable of type String.Normally, String assignments just work, since this behavior is defined in some files shipped with KeY (JavaRedux). However, when generating stubs (that are included via the “bootclasspath” option), the default behavior is overidden by the dummy behavior, resulting in certain elementary things not working.The workaround is to replace the content of the file “” in the folder “stubs/java/lang/” with the content of the “” originally shipped with KeY, and to furthermore add a file “String.key in the same directory (click on the links to download current versions of those files as of 2018/01/25). Now, String assignments should work again.

Other Problems

If you encounter problems not described here, please have a look into our “Getting Help” section.