U ovom poglavlju biće ukratko prokomentarisano nekoliko osnovnih pojmova neophodnih za razumevanje formalne verifikacije programa. Formalna verifikacija programa vrši se u terminima matematičke logike i matematičkih dokaza.
Matematički dokaz je izvođenje neke formule iz skupa aksioma korišćenjem zadatih pravila izvođenja.