First time code in KeY proven with KeY by Mattias Ulbrich