KeY is a deductive verification system for Java programs


Cite this software

What KeY can do for you

KeY - Deductive Java Program Verifier

Tests CodeQL CodeQuality
OpenSSF Best Practices

This repository is the home of the interactive theorem prover KeY for the formal verification and analysis of Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a library e.g. for symbolic program execution, first order reasoning, or test case generation.

For more information, refer to

You can find the releases on GitHub or on Maven Central.

Feel free to use the project templates to get started using KeY:

Help Requests, Issues and Bug Reports

If you encounter problems, feel free to contact us.


  • Hardware: >=2 GB RAM
  • Operating System: Linux/Unix, macOS, Windows
  • Java 17+ since KeY 2.12.0
    • Version 11 for KeY 2.12.0 or older releases
  • Optionally, KeY can make use of the following binaries:

Building KeY

KeY is built with gradle and therefore follows the Maven's standard folder layout.
KeY consists of multiple modules. Modules starting with key. contain a core component of KeY. In contrast, optional extensions start with keyext.. The modules key.util, key.core and key.ui are the base for the product "KeY Prover". Special care is needed if you plan to make changes here.

Obtaining a runnable version of KeY

You can create the single jar-version, aka fat jar, of KeY with ./gradlew :key.ui:shadowJar. The file is generated in key.ui/build/libs/key-*-exe.jar.

Further useful gradle tasks are

  • ./gradlew key.ui:run to start the user interface directly. You can pass program arguments with --args, e.g., ./gradlew key.ui:run --args='--experimental'.

  • Execute all tests with ./gradlew test or ./gradlew testFast. Be aware that this will usually take multiple hours to complete.

Contributing to KeY

Feel free to submit pull requests via GitHub. Pull requests are assessed using automatic tests, formatting and static source checkers, as well as a manual review by one of the developers. More guidelines and documentation for the KeY development can be found under key-docs.

Logo of KeY
Programming languages
  • Java 98%
  • HTML 1%
  • Other 1%
  • GPL-2.0-only
</>Source code

Participating organisations

Karlsruhe Institute of Technology (KIT)
Chalmers University of Technology
Technical University of Darmstadt
University of Koblenz and Landau



Alexander Weigl
Senior Developer
Karlsruhe Institute of Technology
Mattias Ulbrich
Sarah Grebing
Simon Greiner
Christoph Gladisch
Thomas Baar
Christian Engel
Tobias Gedell
Martin Hentschel
Christoph Scheben
Peter Schmitt

Related projects

no image

Core Informatics

A Helmholtz Pilot Program

Updated 3 months ago
In progress