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 Indigo (3.7) or newer.

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

Create a KeY Project

Work with a KeY Project

Inspect verification status

Inspect verification log

Customize build settings

Generated Test Cases

Inspect a counter example

Convert a Java Project into a KeY Project

KeY basics in Eclipse and troubleshooting