KI‑unterstützte formale Verifikation: Von teuren Projekten zur Industrie‑Akzeptanz

Key Takeaway
KI wird die formale Verifikation durch erschwinglichere, automatisierte Beweisskripte und KI‑unterstützte Spezifikationserstellung breit in die Industrie einführen, wodurch Softwareentwicklung von der manuellen Fehlersuche hin zu garantierter Korrektheit übergeht.

Hintergrund

• Formal verification nutzt Tools wie Rocq, Isabelle, Lean, F*, Agda, um mathematisch nachzuweisen, dass Code eine gegebene Spezifikation erfüllt.
• Beispiele: seL4‑Microkernel, Verilog‑basierter C‑Compiler (CompCert), kryptographische Protokollstapel (Everest).

Stand der Technik

• Mehrheit der formalen Systeme bleibt Forschungsprojekt‑dominiert; kaum Industrieanwender, selbst bei hochsicherem Softwarebereich.
• Hoher Aufwand: seL4 erforderte 20 Person‑Jahre, 200.000 Zeilen Isabelle‑Proofs für 8.700 C‑Zeilen.
• Markt‑Kosten: Der erwartete Nutzen von Bug‑Vermeidung ist oft geringer als die Kosten für formale Beweise, weil Fehler als externe Negative Externalitäten gelten.

Auswirkung von LLM‑basierten Programmierassistenten

• LLMs können mittlerweile nicht nur Code, sondern auch Proof‑Scripts in diversen Sprachen generieren.
• Aktuell benötigt ein menschlicher Experte noch Steuerung, aber ein vollständiger Automatisierungsprozess ist naheliegend.
• Proof‑Checker sind kleine, verifizierte Programme, die Fehlschritte zuverlässig aussperren; das macht KI‑generierte Beweise besonders vertrauenswürdig.

Kosten‑ und Nutzen‑Shift

• Automatisierte Vorlagen und LLM‑unterstützte Erstellung reduzieren Kosten drastisch.
• KI‑generierter Code könnte ohne menschliche Überprüfung vertrauenswürdig gemacht werden, wenn die KI selbst beweist, dass er die Spezifikation erfüllt.
• Die größte Herausforderung wird der Definition und Formulierung der Spezifikation selbst sein, obwohl diese Aufgabe bereits relativ leicht und schnell erledigt werden kann.

Zukünftiger Ablauf der Softwareentwicklung

• Hohe‑level‑Deklarative Spezifikation → KI‑generierter Code + nachgewiesene Korrektheit.
• Keine Notwendigkeit, Code manuell zu inspizieren – vergleichbar mit der Abstraktion über Compiler‑generierte Maschinencode.
• Kulturwandel: Industrie muss akzeptieren, dass formale Methoden als praktikabel gelten.

Schlussfolgerung

• Formal verification wird wesentlich günstiger.
• KI‑erzeugter Code erfordert formale Verifikation, um auf Vertrauen zu bauen.
• Die Präzision der formalen Methoden kompensiert die Unsicherheit von LLMs.
• Zusammen führen diese Faktoren zur breiten Akzeptanz in kurzer Zeit, wobei der eigentliche Stillstand nicht technischer, sondern kultureller Natur sein dürfte.

Quelle: Martin Kleppmann