Überprüfung, ob ein Programm einer gegebenen Spezifikation (Spezifikation von Programmen) genügt.

Man unterscheidet unvollständige Verfahren (z.B. Tests auf der Basis mehr oder weniger sorgfältig ausgewählter Anwendungsszenarien) von vollständigen Verfahren.

Eine Möglichkeit einer formalen Programmverifikation besteht in einem mathematischen Korrektheitsbeweis. Ein solcher Beweis arbeitet häufig mit sogenannten Zusicherungen, die Aussagen über den Programmzustand an festgelegten Stellen im Programm treffen. Für verschiedene Typen von Programmbefehlen gibt es leistungsfähige Regeln, die Zusicherungen vor und nach dem jeweiligen Befehl in Beziehung setzen.

Andere formale Verifikationstechniken verwenden Suchverfahren auf dem Zustandsgraphen.