⚠ not yet verified

KeY User Guide

Welcome to the KeY user documentation. This guide covers everything you need to use KeY for the deductive verification of Java programs — from installation to advanced proof scripting. (Information on extending or contributing to KeY lives in the Developer Guide.)

How this guide is organized

The chapters are arranged so that they can be read front to back:

1. Getting Started — install KeY, load a JML-annotated Java program, and run your first proofs. Start here if you are new to KeY.
2. Working with the Prover — day-to-day interactive proving: excluding goals from automation, proof exploration, node diffs, the linearized proof tree, proof caching, and proof slicing.
3. Structuring Verification Projects — the classpath directive, dealing with generics, user-defined data types, and JavaDL escapes in JML.
4. Proof Scripts — make interactive proofs persistent, resilient, and reapplicable with KeY's scripting language.
5. SMT Solvers — how to add and configure SMT solvers.
6. Bridges to Other Tools — exporting proof obligations to Isabelle.
7. Language Reference — the grammars of JML, the KeY input language, and KeY's Java extensions.
8. FAQ — answers to common problems.

The Release Notes list what changed in each KeY release.

Learn more

Additional information is available on the KeY Project homepage or on our GitHub repository, where you can find the source code, development updates, and contribute to the project.

Happy proving!

Disclaimer

Some content of these pages has been co-produced by AI agents, mainly as summaries of other pages, publications or other sources.