KeY prover has been used to verify parts of the OpenJDK library and Norwegian election software, making it one of the most capable tools for formally verifying Java programs. However, an intuitive explanation of its theoretical foundations, capabilities and limitations is not available and the tool itself has a steep learning curve. This greatly increases the amount of effort to understand the tool sufficiently well to evaluate its suitability for ones needs. Here we implement two case studies to develop an intuition for the working of the tool in practice, exploring what properties can or cannot be expressed as specifications and what verifying correctness with KeY means. We find that the learning curve for KeY is even steeper than expected and conclude that it can be used to verify very complex functional and even some non-functional properties of sequential Java 7 code, conditioned on the capabilities of the user.