The main topic of this lecture is a discussion of how to reason about Java interfaces with a particular application to Java’s Collection interface. A new specification method (in the state-of-the-art theorem prover KeY) will be introduced which uses histories that record method invocations and their parameters on an interface. To be discussed are the challenges of proving client code correct with respect to arbitrary implementations, and a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).