Spezifikationen existieren nicht – und das ist ein Problem für die formale Verifikation

Specifications Don't Exist (2025)

Formale Verifikation hat bemerkenswerte Erfolge erzielt, etwa bei Compilern wie CompCert oder Mikrokerneln wie seL4. Doch diese Systeme sind eine kleine, untypische Nische: Für die meisten Software – von Webbrowsern bis zum PDF-Format – existiert keine präzise und kohärente formale Spezifikation, und es gibt Gründe anzunehmen, dass eine solche nie geschrieben werden kann. Der Artikel von Galois untersucht, warum informale Spezifikationen wie Dokumentation, Tests und User Stories die Lücke nicht füllen können, und zeigt am Beispiel PDF, wie selbst ein standardisiertes Format in der Praxis unscharf bleibt. Er argumentiert, dass die eigentliche Hürde für formale Verifikation nicht die Kosten der Beweise sind, sondern die Schwierigkeit, überhaupt zu definieren, was ein System tun soll.