Automatisches Beweisen von Programm-Eigenschaften ist praktisch unmöglich.
(Satz von Gödel, Turing: Halteproblem ist nicht entscheidbar.)
D. h., der Programmierer muß mithelfen: Programm und Beweis gleichzeitig schreiben.
Werkzeuge können verifizieren, daß beides zueinander paßt.
Simples Beispiel: Programm und Typ-Deklarationen.