Taclets and the KeY Prover Martin Giese We give a short overview of the KeY prover, which is the proof system belonging to the KeY tool, from a user interface perspective. In particular, we explain the concept of taclets which is the basic building block for proofs in the KeY prover.