KeY 2.10

KeY 2.10 is the latest stable release and has been published on December 23th, 2021. It comes with many new features under the hood, such as a new SMT translation and completely rewritten parsers for JML and the internal problem and proof format.

In case of questions about KeY please contact:

Download or Start

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

Supported Java and JML Features

Changes in KeY 2.10

  • New ANTLR4 parser for JML
  • New ANTLR4 parser for the internal problem and proof format
  • Rewritten translation of problems to SMT-LIB2 and better communication with SMT solvers (currently supported: CVC4 and Z3)
  • Handling of JML assert/assume-statements via block contracts
  • Tons of bugfixes, for example:
    • fix of a longstanding bug where JML set statements must not be the last statement in a block
    • fix for a completeness gap with array types
    • fixes for various path handling bugs, in particular when working under Windows
  • Full changelog

Previous KeY versions

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

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:

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). 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 (previous 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.