KeY 1.6.5

Run KeY 1.6.5
via Web Start[?]

For getting KeY 1.6.5, choose one of the following options:

New Features in 1.6.5

  • Support for Strings
  • Enhanced JML support
  • Improved integration of external SMT solvers
  • Improved "verification-based testing" mechanism
  • Real Time Java (RTSJ) calculus
  • GUI improvements
  • Various bugfixes
Change log -- Known issues


KeY can optionally use SMT solvers to improve automation:

In addition to directly supporting these solvers, KeY provides an export into the SMT-LIB file format. Bindings for new SMT solvers supporting this format can be added easily, in case of interest please ask the KeY group for assistance.

Examples and Documentation

  • A collection of examples (already included in bytecode and sourcecode distribution):
  • The best source for information on KeY is the KeY Book. In particular, chapter 10 provides a thorough introduction to the system. We provide also updated examples of the KeY Book for KeY-1.6.0 (
  • There are several case studies and tutorials that introduce to the main functions of KeY and show how KeY handles more extensive contexts. In particular, we recommend the KeY Quicktour as an introduction. The examples for the Quicktour can be found here.
  • A cheat sheet for the KeY-Syntax (draft).


KeY is distributed under the GNU General Public License.


Send an email to