(1) En formell teknikk som brukes til å bevise matematisk at et program oppfyller sin angitte requirements.~(2) et bevis på at resultater fra å bruke teknikken i (1).