This course contributes to your abilities to write 100% correct code with the aid of the powerful specification and proving tool Dafny. It increases your knowledge and understanding of tools for static verification of imperative and object-oriented programs.