KeY Resources

KeY Resources provides the “KeY project” with automatic background proofs. Such projects extends the functionality of a Java project by maintaining automatically proofs in background. This means that the tool tries to do proofs automatically whenever files in a project change. Markers are used to show the proof result directly in the source editor. 

The following sections illustrate the main features of KeY Resources using screenshots. Each section contains numbered screenshots that explain a usage scenario step by step. Clicking on each picture produces a more detailed view. The screenshots may differ from the latest release. 


KeY Resources is compatible with Eclipse Mars or newer.

Required update-sites and installation instructions are available in the  download area.

Create a KeY Project

Create a KeY Project

1. Open new project wizard via Package Explorer context menu item “New, Project…”

Select  KeY Project

2. Select “KeY Project”

Define project

3. Define project name and finish the wizard

Work with a KeY Project

Edit & Save source code

1. Edit source code as normal and save it

Proofs are performed during build

2. During build proofs are automatically executed and results are shown via marker

Proofs managed by IDE (folder proofs)

3. Proofs are automatically maintained in folder “proofs”

Tooltip over proof marker

4. Tooltip of a marker explains the proof state and give hints how to continue

Debug or open proofs

5. Proof files can be opend in KeY or the KeYIDE via a marker by selecting “Open proof” to inspect and finish the proof. In addition, a proof can be inspected in the SED via marker menu item “Debug proof”

Inspect verification status

Select Other Views

1. Select main menu item “Window, Show View, Other…”

Open view "Verification Status"

2. Open view “Verification Status”

Status colors

3. Colors of tree items indicate verification statuses

HTML report

4. HTML report lists tasks and assumptions used by proofs

Inspect verification log


1. Select main menu item “Window, Show View, Other…”


2. Open view “Verification Log”


3. Table shows used settings and times of performed verification tasks

Customize build settings

Customize build settings

1. Open project properties of a KeY project via context menu item “Properties”.

Customize build settings

2. Select properties page “KeY, KeY Proof Management” and customize build settings. E.g. enable counter example and test case generation.

Generated Test Cases

Generated Test Cases
1. Generated test cases are maintained in an additional Java project.
In addition, a test suite which executes all test cases is generated.

Inspect a counter example

Inspect a counter example
1. Counter examples can be opend via a marker by selecting “Show Counter Examples”.
Inspect a counter example
2. Inspect the opened counter example.

Convert a Java Project into a KeY Project

Convert a Java Project into a KeY Project
1. Select “Convert to KeY Project” in the context menu of a Java project.
Convert a Java Project into a KeY Project
2. Proofs are automatically maintained
after conversion.

KeY basics in Eclipse and troubleshooting