This chapter is a self-contained introduction into the usage of the
KeY prover, a tool for proving formulas of a program logic called
Java Dynamic Logic. It does not assume the reader to have read any
other chapter of the book in advance. Here, we discuss the usage of
the KeY prover in isolation. For a tutorial on the most common
context of the prover, i.e., the KeY verification process, we refer
to the chapter `Formal Verification with KeY: A Tutorial'. The
present chapter takes entirely the user's perspective on the KeY
prover, and the GUI plays an important role. However, we do not only
introduce the various ways of using, and interacting with, the KeY
prover. Rather, the various visible artifacts the prover acts on, in
particular the logic and the taclet language, are introduced on the
side, on demand, and example driven, in a light-weight manner. This
chapter is meant to be read with the KeY system up and running, such
that every step can be tried out immediately in the system. The
concepts that will be introduced along with the usage of the prover
include KeY problem files, propositional, first-order, and dynamic
logic, sequent calculus, proof construction, proof navigation and
manipulation, taclets, interactive and automated proving, quantifier
instantiation, and symbolic execution. Most of these topics are
discussed in much greater detail in other chapters within this book,
but appear here in the context of using the KeY prover.