KeY is a deductive verification system for Java programs
This repository contains the interactive theorem prover "KeY" for the verification of Java programs.
You can find more information about KeY on https://key-project.org or use the documentation in the companion repository key-docs. The content of the latter is also available as HTML version under https://key-project.org/docs.
The current version of KeY is 2.10.0, licensed under GPL v2.
This folder provides a gradle-managed project following
Maven's standard folder layout.
There are several subprojects in this folder. In general, every
key.*/ subproject contains a core component of KeY.
Additional and optional components are in
keyext.*/ folders. The file
build.gradle is the root build script
describing the dependencies and common build tasks for all subprojects.
key.ui are the base for the product "KeY Prover". Special care is needed
if you plan to make changes here.
Assuming you are in the directory of this README file, you can create a runnable and deployable version with one of these commands:
./gradlew key.ui:run you can run the user interface of KeY directly from the repository.
./gradlew key.ui:run --args='--experimantal' to enable experimental features.
./gradlew classes to compile KeY, which includes running JavaCC and Antlr.
./gradlew testClasses if you also want to compile the JUnit test classes.
Test your installation with
./gradlew test. Be aware that this will usually take multiple hours to complete.
./gradlew testFast, you can run a more lightweight test suite that should complete in a few minutes.
You can select a specific test case with the
--tests argument. Wildcards are allowed.
./gradlew :key.<subproject>:test --tests "<class>.<method>"
You can debug KeY by adding the
--debug-jvm option, then attaching a debugger at
You can create a single jar-version, aka fat jar, of KeY with
The file is generated in
A distribution is build with
./gradlew :key.ui:installDist :key.ui:distZip
The distribution can be tested by calling
and is zipped in
The distribution gives you potential of using single jar files.
Quality is automatically assessed using SonarQube on each merge requests. The results of the assessments can be found on SonarCloud.io (Branches).
The rules and quality gate are maintained by Alexander Weigl firstname.lastname@example.org currently.
More guideline and documentation for the KeY development can be found under key-docs.
If you encounter problems, please send a message to
This is the KeY project - Integrated Deductive Software Design Copyright (C) 2001-2011 Universität Karlsruhe, Germany Universität Koblenz-Landau, Germany and Chalmers University of Technology, Sweden Copyright (C) 2011-2022 Karlsruhe Institute of Technology, Germany Technical University Darmstadt, Germany Chalmers University of Technology, Sweden The KeY system is protected by the GNU General Public License. See LICENSE.TXT for details.