This recitation covered contracts and had an intro to correctness proofs.
Handout (Solutions, Code)