Getting Started

Download KeY

• Download the latest stable version of KeY as single click jar and double-click the jar file (or use java -jar key-2.x.x-exe.jar on the command line).
• Alternatively, you can download the latest development version.

Tutorials & Examples

Load an example from the list presented in the dialog that pops up when starting KeY. Good choices are, e.g.:

• “Quicktour” for program verification
• “Transitivity of Subset” for first-order logic
• “Declassification – Sum” for information flow analysis

Take a look at our tutorials section for program verification. A good starting point is the tutorial on formal verification with KeY in the KeY book. The examples from the book are available here.

KeY as a Library

You can use KeY as a library in your own project: Make use of its capabilities as a first-order prover or symbolic execution engine. We provide some starting points for you in the “KeY for Your Own Research Projects” section. Download the KeY nightly source code distribution here and take a look at our documentation documentation.

Getting Help

The preferred way for getting help, in particular when you want to use KeY as a library or want to change or extend the source code, is to use StackOverflow. Be sure to tag your question with the key-formal-verification tag, so that your question is not lost amongst all the questions on StackOverflow. Alternatively, you can write an email to our mailing list support@key-project.org.