KeY 2

KeY 2.4.1 is the latest stable release, released on February 19, 2015.

KeY 2 differs significantly from the previous KeY 1.6 release. The older KeY 1.6 release is currently still maintained and available as KeY 1.6.5 (released on April 18, 2013).

KeYmaera and other KeY variants like KeY-Hoare can be found here.

Download or Start

Run KeY 2.4.1
via Web Start[?]
KeY requires Java version 6 or newer and is tested on Linux, OS X and Microsoft Windows.

New Features in 2.x

  • Explicit Heap Model and Dynamic Frames
  • Verification of Recursive Methods
  • Further Enhancend JML Support (Details)
  • Simplified representation of integers
  • GUI improvements (refreshed appearance, improved search, keyboard shortcuts
  • Counter Example Generation & Test Generation
  • Calculus for Information Flow Reasoning
  • Full support for shift-operations and partially for other binary operators
  • Various bugfixes

KeY-Based Eclipse Projects

Add the best matching update-site to your Eclipse release to install the listed KeY-based projects:

KeY 2.4.1 for Eclipse 4.4 (Luna)
Update Site Name: KeY Luna Updates
Update Site URL:
KeY 2.4.1 for Eclipse 4.3 (Kepler)
Update Site Name: KeY Kepler Updates
Update Site URL:
KeY 2.4.1 for Eclipse 4.2 (Juno)
Update Site Name: KeY Juno Updates
Update Site URL:
KeY 2.4.1 for Eclipse 3.7 (Indigo)
Update Site Name: KeY Indigo Updates
Update Site URL:
Project Explanation Category Status
KeY 4 Eclipse Starter A basic Eclipse extension to start KeY from within Eclipse. Verification Release
KeYIDE An alternative user interface for KeY directly integrated into Eclipse. Verification Beta
KeY Resources Provides the "KeY project" with automatic background proofs. Verification Release
MonKeY Batch verification of all proof obligations. Verification Release
Symbolic Execution Debugger (SED) A debugger based on symbolic execution. Debugging Release
Visual DbC A proof management and visualization tool. Visualization Release

JML Editing and Stubby are available on the preview update site.

For an optimal user experience it is recommended to use at least the following JVM memory settings:

  • -Xms128m
  • -Xmx1024m
  • -XX:MaxPermSize=256m

They can be changed in the "eclipse.ini" file or by starting Eclipse with the following additional parameters:
-vmargs -Xms128m -Xmx1024m -XX:MaxPermSize=256m


KeY can optionally use SMT solvers to improve automation:

In addition to directly supporting these solvers, KeY provides an export into the SMT-LIB file format. Bindings for new SMT solvers supporting this format can be added easily, in case of interest please ask the KeY group for assistance.



KeY is distributed under the GNU General Public License.


Send an email to

Feature Preview of KeY-Based Eclipse Projects

The following update-site is based on newer KeY versions and offers a preview of future features. Due to the non final status, productive use is not recommended.

Previews for Eclipse 4.4 (Luna), Eclipse 4.5 (Mars) and Eclipse 4.6 (Neon)
Update Site Name: KeY Luna Updates
Update Site URL:
Project Explanation Category Status
JML Editing JDT extension to support JML. Editing Beta
Stubby Stub Generation of used API members. Utilities Beta

Unstable development builds (nightly builds)

Run nightly build
via Web Start[?]
No support is provided for development versions.

Older Releases

Older releases with sources and appropriate older versions of external libraries.