It is in use for undergraduate courses in the universities that develop it, and I used it too. It ships with small training problems. What would you like to kno

It is in use for undergraduate courses in the universities that develop it, and I used it too. It ships with small training problems. What would you like to know? There are many documents on JML. The prover works for you, you just left click logic expressions in KeY and you can prove large parts by point-and-click. It can also finish proofs for you if it's trivial. Often, you only need to specify the loop invariants. I'd recommend opening up KeY, loading one of the trivial examples first: Contraposition. This will be a quick reminder on the logic concepts like implication, but you pretty much cannot screw it up. Try to understand why the proof tree branches when you choose certain steps. Afterwards, try something else from "Getting started" like the examples that the proof searcher can prove (for example SumAndMax) and exploring the proof tree, and trying out yourself from scratch. The automatic proofs are not always pretty, so it's more for to do the manual work first. KeY will only let you do valid proof steps, so you learn quickly how proofs work.