In this 30 minute session, we show how to prove the correctness of the method contract of unlinkLast of java.util.LinkedList using the KeY prover. The method contract is specified using JML (not shown in video).