Formal verification involves using mathematical techniques to prove that computer programs satisfy certain properties. There are three main techniques: input-output assertions use predicates associated with code points to show relations will hold; weakest preconditions work backwards from desired outputs to find necessary inputs; and structural induction proves properties by showing they hold for base cases and are preserved as the structure increases in size. The document provides examples and explanations of each technique.