Skip to content
⚠ not yet verified

Developer Guide

This guide is for developers who want to work on KeY or build on top of it. (If you want to use KeY to verify programs, see the User Guide instead.)

How this guide is organized

  1. Architecture — how the code base is organized into Gradle modules and where the important packages live. Read this first.
  2. Building KeY — checking out, building, running, and testing KeY with Gradle.
  3. Working on the Code — coding conventions, automatic formatting with Spotless, and logging; see also CONTRIBUTING.md in the repository.
  4. Extending KeY — the central chapter for adding functionality. It starts with a decision table ("I want to add …") and contains compiled, verified How-Tos for the most common tasks: a new extension module, a menu entry, a toolbar, taclets, a proof macro, and a script command. In-depth references: writing taclets, polarity triggers, GUI extension points, script commands, SMT solvers, and event listeners.
  5. Using KeY as a Library — KeY in external projects and the JSON-RPC interface.
  6. Internals — background on selected subsystems: the rule application pipeline (taclet matching → strategy evaluation → application), proof loading/saving, the KeY parser, SMT translation, and counterexample generation.
  7. Testing — unit tests, RunAllProofs, proved rules, CI.
  8. Writing Documentation — how to contribute to this site.

Dependencies worth knowing