Formale Methoden sind mathematisch rigorose Techniken, um Software-Eigenschaften für alle möglichen Eingaben zu beweisen, nicht nur für ausgewählte Testfälle. Sie reichen von Typsystemen über Model-Checking bis zu Beweisassistenten wie Isabelle. Damit lassen sich Garantien formulieren, die durch Tests grundsätzlich nicht erreichbar sind, etwa dass Geld bei jeder denkbaren Transaktionsunterbrechung nicht verloren geht.
Das Wichtigste in Kürze
- Testen kann Fehlerfreiheit grundsätzlich nicht beweisen, weil Tests immer nur endlich viele Beispiele abdecken, nie alle möglichen Eingaben.
- Formale Methoden skalieren von leichtgewichtigen Typsystemen bis zu vollständigen mathematischen Beweisen mit Werkzeugen wie Isabelle oder Model-Checkern.
- Wer formale Verifikation plant, muss sie von Anfang an in den Entwicklungsprozess einbauen, nachträgliches Draufsetzen funktioniert nicht.
- Verifizierter Code ist kein Ersatz für Tests: Der verifizierte C-Compiler CompCert prüft nur den Compiler-Kern, die Randbereiche werden zusätzlich per Fuzzing abgesichert.
- KI-gestützte Beweissuche, etwa der Sledgehammer in Isabelle, ist in formalen Systemen risikolos, weil jeder generierte Beweis automatisch nochmal unabhängig geprüft wird.
Warum Testen Fehlerfreiheit nicht garantieren kann
Testen liefert Beispiele, keine Beweise. Wer einen Testfall durchspielt, prüft genau eine Konstellation. Danach folgt der zweite, der dritte, vielleicht der fünfte Fall. Was bleibt, ist eine Liste von Stichproben, nie eine Aussage über alle möglichen Eingaben.
Edsger Dijkstra hat das schon formuliert: Mit Tests lässt sich die Anwesenheit von Fehlern zeigen, nicht deren Abwesenheit. Für viele Anwendungen reicht das. Für manche nicht.
In Zahlungssystemen, in Automotive oder in der Medizin gibt es Eigenschaften, die für jede denkbare Konstellation gelten müssen. Ein Beispiel aus dem Zahlungsverkehr: Eine Karte wird per NFC angehalten, dann reißt die Verbindung ab. Egal wann das passiert, die Transaktion muss zurückrollbar und wiederholbar sein, ohne dass Geld verloren geht. Diese Garantie gilt für alle Abbruchzeitpunkte. Ein Stichproben-Test deckt sie nicht ab.
Was formale Methoden leisten
Formale Methoden denken mathematisch rigoros über Software nach. Statt einzelner Testfälle wird das System strikt modelliert, und Eigenschaften wie Invarianten werden so formuliert, dass sie Aussagen über alle möglichen Eingaben und Ausgaben treffen.
Der Computer übernimmt dabei die Rolle des Prüfers. Bei einem Beweisassistenten weist die Maschine nach, dass der geführte Beweis keine Lücken enthält, keine falschen Schlüsse, nichts Weggelassenes. Das Ergebnis ist eine Garantie, dass der Worst Case nicht durchrutschen kann.
Bianca Lutz bringt den Kern auf den Punkt: Es geht um die Garantie, dass es den Worst Case gar nicht geben kann, und um den Nachweis dieser Garantie. Genau dort setzen formale Methoden an, wo Testen prinzipiell aufhört.
Formale Methoden sind kein Alles-oder-nichts
Zwischen vollständigem Beweis und gar keiner Formalisierung liegt ein breites Spektrum. Die leichtgewichtigste formale Methode benutzen die meisten Entwickler täglich, ohne sie so zu nennen: das Typsystem.
Ein Typchecker sagt mit Sicherheit, dass ein Wert ein String ist und keine Zahl, und das für alle Aufrufe einer Funktion. Das Ergebnis kommt fast umsonst, der Checker läuft einfach mit. Dafür ist die Aussage begrenzt: Über die Korrektheit des Verhaltens sagt ein Typ wenig.
Wer über Korrektheit reden will, muss tiefer in die Semantik des Systems gehen. Die Abstufungen reichen vom Typsystem über Model-Checker bis zum vollständigen Beweisassistenten. Mehr Ausdrucksmächtigkeit bedeutet mehr Aussagekraft, aber auch mehr Aufwand.
Diese Übersicht ordnet die Ebenen nach Aufwand und Aussagekraft:
| Ebene | Aufwand | Aussage |
|---|---|---|
| Typsystem | sehr gering, läuft mit | begrenzt, z. B. String statt Zahl |
| Model-Checking | gering bis mittel, hoch automatisiert | findet verbotene Pfade, Gegenbeispiele |
| Beweisassistent (z. B. Isabelle) | hoch, oft manuell | vollständiger Korrektheitsbeweis |
Wie viel Aufwand ein vollständiger Beweis kostet
Vollständige Verifikation ist teuer. Beim verifizierten Mikrokernel seL4, der mit dem Tool Isabelle bewiesen wurde, liegt der geschätzte Overhead je nach Programmiersprache bei einem Faktor von 10 bis 100. Bei Faktor 10 heißt das: Jede Zeile Code erfordert zehn Zeilen Beweis.
In der Praxis ist das eine harte Ansage an die Projektplanung. Ein Feature, das zwei Monate Entwicklung gekostet hat, kann zwei zusätzliche Jahre für die Validierung bedeuten. Ob sich das lohnt, hängt vom Leidensdruck und der Kritikalität ab.
Deshalb ist die volle Verifikation selten der richtige Default. Sinnvoller ist die Frage, welche Ebene für den konkreten Anwendungsfall passt und wie viel du zu investieren bereit bist. Der Vergleich zu Testabdeckung trägt: 80 Prozent sind besser als 0, und manchmal reicht 80 Prozent völlig.
Verifikation gehört in die Entwicklung, nicht dahinter
Formalisierung funktioniert nicht als nachgelagerte Prüfung. Die Vorstellung, ein fertiges Programm über den Zaun zu Spezialisten zu werfen, die dann Korrektheit zeigen, geht an der Realität vorbei.
Am Beispiel seL4 wird sichtbar, warum. Wer Verifikation früh mitdenkt, bekommt schon während der Entwicklung Feedback von jemandem, der abstrakter über die Domäne nachdenkt. Daraus entstehen Hinweise auf interessante Systemeigenschaften oder die Empfehlung, auf eine Sonderlocke zu verzichten, weil sie im allgemeinen Fall bestimmte Garantien zerstört.
Das verändert den Entwicklungsprozess zum Besseren. Nur wenn der Beweis von Anfang an mitläuft, lässt sich ein System bauen, das funktional ausgereift und zugleich dem Beweis zugänglich bleibt.
Automatisch oder manuell: das ganze Spektrum
Es gibt nicht das eine Verifikationstool, sondern zig verschiedene, von vollautomatisch bis vollständig manuell. Welches passt, hängt von der Eigenschaft ab, die du nachweisen willst.
Ein automatisiertes Beispiel sind Treiber unter Windows. Microsoft prüft die mitgelieferten Treiber auf Korrektheitseigenschaften, etwa darauf, dass keine Endlosschleifen und keine Nullpointer-Zugriffe entstehen. Der Hersteller liefert C- oder C++-Code, automatisierte Werkzeuge analysieren ihn statisch.
Manchmal brauchen diese Tools Unterstützung. Bei einer nicht-trivialen While-Schleife hilft ein maschinenlesbarer Kommentar, der etwa festhält, dass ein Counter in jedem Durchlauf verringert wird. Dann prüft das Tool nur noch, ob der Counter sinkt, und erkennt die Terminierung.
Dieser Ansatz ist nah am Code, der wirklich ausgeführt wird. Das ist der Goldstandard, aber er beweist nur, was er beweist: dass der Treiber nicht crasht, nicht dass er tut, was er soll.
Modell, Spezifikation und Code sind verschiedene Dinge
Korrektheit hat mehrere Bezugspunkte. Wer ein abstraktes Modell des Algorithmus aufschreibt und in einem formalen Tool implementiert, prüft nicht den echten Code, sondern das Modell. Trotzdem ist das meist hilfreich, weil viele Fehler schon in der Spezifikation beginnen.
Das Muster kennt jeder: Eine User-Story klingt einfach, bis man darüber nachdenkt, was in den Grenzfällen herauskommen soll. Ein durchdachtes Modell deckt diese Lücken auf, bevor Code entsteht.
Die entfernteste Ebene ist die reine Spezifikation, formuliert in natürlicher Sprache und ergänzt um einige Formeln. Auch das schärft das Verständnis, selbst wenn am Ende die Implementierung vom Modell abweichen kann.
Kugelsicher heißt nicht unverwundbar
Formale Methoden sind keine Silver Bullet. Sie ersetzen nicht jede andere Maßnahme, und nicht alles ist danach automatisch bewiesen und schön. Sie sind eine Bereicherung, um das System besser zu verstehen und zu einer tragfähigen Spezifikation zu kommen.
Der verifizierte C-Compiler CompCert zeigt die Grenze konkret. Verifiziert ist der Compiler-Kern. Die Übersetzung am Eingang und der Schritt zum echten Maschinencode am Ausgang sind nicht formalisiert. Diese Ränder lassen sich mit Compiler-Fuzzing absichern, das randomisierte C-Programme durchschickt, oder durch eine zweite Referenzimplementierung zum Vergleich.
Mein Kopf ist nach wie vor nicht geschützt, aber mein ganzer Torso, eine sehr große Fläche, ist abgedeckt. Damit bin ich sicherer als ohne das.
Bianca Lutz
Das Bild der kugelsicheren Weste trägt: Sie deckt eine große Fläche ab, nicht den ganzen Körper. Verifikation und Testen ergänzen sich, statt sich auszuschließen.
Eine einfache Implementierung neben der komplexen
Performante Implementierungen sind selten offensichtlich korrekt. Es gibt zwei Wege: Entweder ein System ist so einfach, dass es offensichtlich keine Fehler gibt, oder so komplex, dass es keine offensichtlichen Fehler gibt. Meist braucht man die komplexe Variante, weil Performance oder andere Anforderungen es verlangen.
Daraus folgt eine pragmatische Technik. Stell der komplexen, schnellen Implementierung eine einfache, langsame zur Seite und vergleiche beide. Wenn der Vergleichslauf eine Stunde dauert, ist das verschmerzbar, solange die performante Variante nachweislich korrekt arbeitet.
Was Änderungen am verifizierten System kosten
Der Aufwand einer Änderung hängt davon ab, wo sie ansetzt. Ändert sich nur ein Implementierungsdetail, ohne dass sich die Garantien ändern, etwa ein effizienterer Algorithmus innerhalb eines Moduls, reicht meist eine lokale Anpassung.
Verschärfend wirkt die fehlende Modularität der Beweise. Im Gegensatz zu Software gibt es kein echtes Information Hiding, weil man über die Interna sprechen können muss. Eine Datenstruktur, über die man später etwas beweisen will, lässt sich nicht hinter einer losen Kopplung verstecken.
Wer eine basale Definition ändert, spürt das durch die gesamte Beweisbasis. Bianca berichtet von einem Jahr Arbeit, um nach einer solchen Änderung alle Beweise auf die neue Sprache nachzuziehen.
Ein konkretes C-Problem ist der gemeinsame Speicher. Weil in C im Prinzip jeder in jeden Speicher schreiben kann, muss erst bewiesen werden, dass Modul A nicht in den Bereich von Modul B schreibt. Dafür gibt es die Separation Logic mit getrennten Heap-Bereichen. Ändert sich die Pointer-Struktur, sind die Separations-Beweise neu zu führen. In einer funktionalen Sprache tritt dieses Problem gar nicht erst auf.
KI hilft beim Beweisen, ohne dass man ihr glauben muss
Maschinelles Lernen unterstützt das Beweisen seit über zehn Jahren, lange bevor man es KI nannte. In Isabelle hilft das Werkzeug Sledgehammer, Beweise schneller zu schreiben.
Sledgehammer sucht aus dem Kontext relevante Fakten heraus, ähnlich einer IDE, die eine passende Methode vorschlägt, und wirft sie in automatische Beweis-Tools. Maschinelles Lernen erkennt dabei, welche Fakten erstaunlich häufig funktionieren, und schlägt sie öfter vor. Die Hauptaufgabe ist, dem Punkt vorzubeugen, an dem der Computer die Suche abbricht, weil er sonst nicht fertig wird.
Der entscheidende Vorteil: Beweisen ist der ideale Anwendungsfall für KI, weil das Ergebnis unabhängig überprüft wird. Halluzinationen sind kein Problem. Stimmt ein generierter Beweis nicht, lehnt der Beweis-Checker ihn ab, und man versucht es erneut.
Isabelle glaubt seiner eigenen KI nicht.
Bianca Lutz
Egal welches krude Zeug aus einem Sprachmodell fällt, es wird ohnehin nochmal geprüft. Genau deshalb darf man bei der Beweissuche bedenkenlos wild vorgehen: Das Sicherheitsnetz prüft jeden Vorschlag gegen die Logik des Systems.
