Formale Verifikation

Normalerweise prüft man Software durch Testen. Man probiert einige Eingaben aus und schaut, ob das Ergebnis stimmt. Das findet viele Fehler, aber nie alle: getestet wird immer nur ein winziger Teil aller denkbaren Fälle. Formale Verifikation geht anders vor. Man schreibt exakt auf, was das Programm leisten soll, und beweist mathematisch, dass es das immer tut. Der Beweis gilt dann für jede mögliche Eingabe, nicht nur für die ausprobierten. Der Unterschied ist wie zwischen zwanzig Rechenbeispielen und einem Beweis in der Mathematik.

Warum das wichtig ist

Manche Fehler darf man sich nicht erlauben. Die Steuersoftware eines Flugzeugs, die Bremsen eines Zuges, ein Herzschrittmacher: hier kostet ein Absturz Menschenleben. Auch bei Prozessoren ist es teuer. Ein Rechenfehler im Chip lässt sich nach der Produktion nicht per Update reparieren, sondern nur durch Rückruf.

In der Kryptographie ist die Lage ähnlich. Ein Verschlüsselungsprogramm kann bei 99,9 Prozent der Eingaben korrekt arbeiten und trotzdem unbrauchbar sein. Angreifer suchen genau den einen Fall, der nicht funktioniert. Testen hilft dagegen wenig, ein Beweis schon.

Seit KI-Systeme wichtige Entscheidungen treffen, wird die Frage neu gestellt. Ein Sprachmodell selbst kann man nicht formal verifizieren, dazu ist es zu groß und zu unscharf definiert. Aber man kann die Software drumherum beweisen, die das Modell überwacht und begrenzt.

Wie es funktioniert

Der erste Schritt ist die Spezifikation. Sie beschreibt in einer präzisen, mathematischen Sprache, was gelten soll. Zum Beispiel: das Ergebnis dieser Sortierfunktion ist immer aufsteigend geordnet und enthält genau die gleichen Elemente wie die Eingabe. Dieser Schritt ist oft der schwerste, weil man erst hier merkt, wie unklar die eigenen Anforderungen waren.

Dann kommt der Beweis. Dafür gibt es Programme, die Beweisassistenten heißen, etwa Coq, Isabelle oder Lean. Der Mensch gibt die Beweisidee vor, das Programm prüft jeden Schritt auf Lücken. Es akzeptiert nichts, was nicht wirklich folgt.

Für einfachere Eigenschaften geht es auch automatisch. Ein Model Checker durchsucht systematisch alle erreichbaren Zustände eines Systems und meldet, wenn einer davon die Regel verletzt. Solche Werkzeuge finden Fehler, die Menschen übersehen, weil sie stur jede Kombination durchgehen.

Der Aufwand ist der Preis. Für ein bewiesenes Programm braucht man leicht das Zehnfache an Arbeit gegenüber normalem Code. Deshalb verifiziert niemand eine ganze App, sondern nur den kritischen Kern.

Wo man dem Begriff begegnet

Intel und AMD setzen formale Verifikation seit Jahrzehnten in der Chipentwicklung ein. Auslöser war ein Rechenfehler in einem Pentium-Prozessor von 1994, der Intel einen dreistelligen Millionenbetrag kostete. Heute wird jede Recheneinheit vor der Produktion mathematisch geprüft.

Bekannte Beispiele aus der Software sind der Betriebssystemkern seL4 und der C-Compiler CompCert. Beide sind vollständig bewiesen und werden dort verwendet, wo Zulassungsbehörden harte Nachweise verlangen, etwa in der Luftfahrt.

In News zu Kryptowährungen taucht der Begriff bei Smart Contracts auf. Das sind Programme, die automatisch Geld verwalten. Weil Fehler dort direkt zu Verlusten führen, lassen manche Projekte ihren Code formal verifizieren und bewerben das als Sicherheitsmerkmal. Ein Beweis deckt allerdings nur ab, was in der Spezifikation steht. Ist die Anforderung falsch formuliert, ist auch der Beweis wertlos.