Traditionally, KeY was a program verification tool for Java. Although this still is one of its main applications, it grew over the years to a program verification platform with various fields of application. The currently most prominent applications are:

We are constantly working on making the KeY framework more accessible for other applications. For instance, it is quite easy to use KeY as a symbolic execution engine in the backend of another tool. Ongoing work includes, for instance, the construction of a Java compiler based on symbolic execution trees created by KeY.