
Do not attempt a full formal correctness proof from the beginning.

Start with abstract specification languages (e.g. set theory) based on first-order logic.

Learn to formally specify.

Put the verification of code aside for later, focus on writing good models.

Abstract away cryptography, assume it is correct, focus on functional specifications.

Add lightweight or automated verification techniques such as simulation [1]}, prototyping [2]}, model-based testing [3]}, model-checking [4]} and automated proofs [5]}, [6]}.

Assess what you have learned, correct the course and move on.

