Formale Verifikation: 50 Jahre alte Argumente auf dem Prüfstand

The Case Against Formal Verification, 50 Years Later

Die Begeisterung für formale Verifikation wächst, angetrieben durch KI-Codierung. Ein Rückblick auf das Paper "Social Processes and Proofs of Theorems and Programs" von 1979 zeigt, welche Argumente gegen die Verifikation heute noch Bestand haben. Der Autor analysiert sechs Einwände – von Spezifikationsproblemen bis zur Unmöglichkeit vollautomatischer Verifikation – und bewertet sie im Licht moderner Entwicklungen wie LLM-gestützter Beweisführung und Coding-Agents. Fazit: Formale Methoden sind kein Allheilmittel, aber wertvoll für Verständnis und Korrektheit, besonders wenn KI Code schreibt.