We present the state of the art in the KeY Java theorem prover, which is based on a first-order object-oriented dynamic logic.This assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from aspecific implementation of object creation. Objects which are not (yet) created never play any role. Corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and the proof rules is illustrated by means of an example of a reachability property of a linked list. All proof rules presented are fully implemented in a special version of KeY.