We present the contents of a new formal methods course taught to undergraduate students in their third year at the University of Rennes 1 in France. This course aims at initiating students to formal methods, using the Why3 platform for deductive verification. It exposes students to several techniques, ranging from testing specifications, designing loop invariants, building adequate data structures and their type invariants, to the use of ghost code. At the end of the course, most of the students were able to prove correct in an automated way non-trivial sorting algorithms, as well as standard recursive algorithms on binary search trees.