KeY: A Formal Method for Object-Oriented Systems Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Peter H. Schmitt This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented software. It aims for integrating design, implementation, formal specification and formal verification as seamlessly as possible. The intention is to provide a platform that allows close collaboration of conventional and formal software development methods.