(1) Μια επίσημη τεχνική που χρησιμοποιείται για να αποδεικνύουν μαθηματικά ότι ένα πρόγραμμα υπολογιστή πληροί την καθορισμένη requirements.~(2) μια απόδειξη που προκύπτει από την εφαρμογή της τεχνικής (1).