The KeY project is a long-term research project started in 1998 by Reiner Hähnle, Wolfram Menzel, and Peter Schmitt at University of Karlsruhe (now Karlsruhe Institute of Technology). After Menzel’s retirement, Bernhard Beckert joined the project leader team, which has been unchanged ever since. (…) From the very first publication [Hähnle et al., 1998] the aim of the KeY project was to integrate formal software analysis methods, such as formal specification and formal verification, into the realm of mainstream software development. This has always been—and still is—a very ambitious goal that takes a long-time perspective to realize. (…) From the mid 2000s onward, a number of application scenarios for deductive verification technology beyond functional verification have been realized on the basis of the KeY system. These include test case generation, an innovative debugging tool, a teaching tool for Hoare logic, and an Eclipse extension that integrates functional verification with mainstream software development tools. Even though they share the same code base, these tools are packaged separately to cater for the different needs of their prospective users.