KeYIDE is an alternative user interface for KeY directly integrated into Eclipse. The goal of this project is to provide the same functionality as the original user interface of KeY. Up to now only the basics (proof tree navigation, auto mode, interactive rule application) are available.

The following sections illustrate the main features of the KeYIDE 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.


The KeYIDE is compatible with Eclipse Indigo (3.7) or newer.

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

Verify a method contract

Start auto mode

Stop auto mode when breakpoint is hit

Apply a rule interactively

Generate a counter example

Generate test cases

KeY basics in Eclipse and troubleshooting