VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

Das Paper stellt VeriStruct vor, ein Framework, das KI-gestützte automatische Verifikation von komplexen Datenstruktur-Modulen in Verus durch einen Planer, syntaktische Leitlinien und eine Reparaturphase ermöglicht und dabei in Tests eine Erfolgsrate von 99,2 % bei der Verifikation von Funktionen erreicht.

Das Wesentliche

Stellen Sie sich vor, Sie bauen ein riesiges, komplexes Haus aus Lego. Sie haben die Steine (den Code) und Sie wissen, wie das Haus am Ende aussehen soll (die Tests). Aber es gibt ein Problem: Bevor Sie das Haus wirklich fertigstellen, müssen Sie beweisen, dass es nicht einstürzt, wenn ein Windstoß kommt oder wenn jemand ein Fenster aufmacht.

Normalerweise müssten Sie als Architekt für jeden einzelnen Stein und jede Verbindung eine schriftliche Erklärung verfassen, warum das sicher ist. Das ist extrem mühsam, langweilig und erfordert ein Genie für Mathematik.

VeriStruct ist wie ein super-intelligenter Assistent, der Ihnen hilft, diese Beweise automatisch zu schreiben – und zwar für ganze Module (wie ein ganzer Baustein-Set für ein Regal oder eine Treppe), nicht nur für einen einzelnen Stein.

Hier ist die Geschichte von VeriStruct, einfach erklärt:

1. Das Problem: KI ist klug, aber manchmal verwirrt

Künstliche Intelligenz (KI) kann heute sehr gut Code schreiben. Aber wenn es darum geht, formale Beweise zu schreiben (also mathematische Garantien, dass der Code sicher ist), stolpert die KI oft.

• Die Sprache: Die KI spricht zwar "Code", aber die Sprache für Beweise (hier "Verus") hat sehr spezielle Regeln. Es ist, als würde die KI versuchen, ein juristisches Dokument auf Latein zu schreiben, aber sie verwechselt ständig die Rechtschreibung.
• Die Komplexität: Ein einzelner Code-Befehl ist einfach. Aber eine ganze Datenstruktur (wie ein Ringpuffer, der Daten speichert) ist wie ein komplexes Uhrwerk. Die KI versteht oft nicht, wie die Teile zusammenhängen, wenn sie nicht genau erklärt wird.

2. Die Lösung: VeriStruct – Der Bauleiter mit einem Plan

VeriStruct ist kein einfacher "Schreib-Assistent". Es ist ein Workflow-System, das wie ein erfahrener Bauleiter agiert. Es teilt die Aufgabe in kleine, überschaubare Schritte auf.

Stellen Sie sich den Prozess wie das Bauen eines Hauses vor:

Schritt A: Der Architekt (Der "Planner")

Bevor die KI anfängt zu schreiben, schaut sich ein "Planer" den Code an. Er fragt sich: "Brauchen wir hier überhaupt eine spezielle mathematische Abstraktion? Brauchen wir eine Regel, die sagt, dass die Tür immer geschlossen bleibt?"

• Analogie: Wenn Sie ein einfaches Regal bauen, brauchen Sie keine Statik-Berechnung für ein Hochhaus. Der Planer entscheidet, welche Werkzeuge (Module) wir wirklich brauchen, damit wir nicht unnötig viel Arbeit machen.

Schritt B: Die Spezialisten (Die Module)

Sobald der Plan steht, schickt VeriStruct die KI an verschiedene Spezialisten-Arbeitsplätze:

1. Der Übersetzer (View-Modul): Datenstrukturen sind oft kompliziert im Inneren (wie ein Ringpuffer, der sich wie ein Kreis dreht). Der Übersetzer erfindet eine einfache, mathematische "Landkarte" (eine Abstraktion), die dem Beweis-System sagt: "Vergiss die komplizierte Kreisbewegung, betrachte es einfach als eine Liste von Dingen."
2. Der Sicherheitsinspektor (Typ-Invarianten): Dieser sagt: "Was muss immer wahr sein?" (z. B. "Die Tür darf niemals offen sein, wenn das Licht an ist").
3. Der Vertragsschreiber (Spezifikationen): Er schreibt die Regeln für jede Funktion: "Wenn du das hier tust, passiert garantiert das dort."

Schritt C: Die Korrektur-Station (Repair)

Das ist der wichtigste Teil. Die KI macht Fehler. Sie vergisst ein Komma oder benutzt eine Regel falsch.

• Analogie: Stellen Sie sich vor, Sie bauen das Haus. Der Bauleiter (VeriStruct) schaut sich das Ergebnis an und sagt: "Ups, hier steht 'Tür' statt 'Fenster'. Das wird nicht funktionieren."
• Anstatt alles abzureißen, schickt VeriStruct den Code zurück in die Reparatur-Station. Dort gibt es spezielle Werkzeuge, die genau diesen Fehler erkennen und korrigieren. Dieser Prozess wiederholt sich so lange, bis das Haus stabil ist.

3. Das Ergebnis: Ein fast perfektes Haus

Die Forscher haben VeriStruct an 11 verschiedenen "Häusern" (Datenstrukturen) getestet.

• Das Ergebnis: VeriStruct hat es geschafft, 10 von 11 Häusern vollständig zu beweisen.
• Von insgesamt 129 einzelnen Bauteilen (Funktionen) wurden 128 (99,2 %) erfolgreich verifiziert.
• Zum Vergleich: Ein einfacher KI-Versuch ohne diesen cleveren Planer und die Reparatur-Station hat nur bei 4 von 11 Häusern geklappt.

Warum ist das wichtig?

Früher mussten Menschen stundenlang mühsam diese Beweise schreiben. Das war so teuer, dass es kaum jemand machte.
Mit VeriStruct wird die KI zum Co-Piloten, der die schwere Arbeit der Beweisführung übernimmt. Sie müssen nur noch den Code und ein paar Tests liefern, und das System baut die Sicherheitsgarantien drumherum.

Zusammenfassend:
VeriStruct nimmt die KI, die manchmal chaotisch ist, und gibt ihr einen Bauplan, Spezialisten für verschiedene Aufgaben und eine Korrektur-Station. So wird aus einem chaotischen KI-Versuch ein präzises, sicheres System, das uns hilft, Software zu bauen, die wir wirklich vertrauen können.

Technische Zusammenfassung

1. Problemstellung

Die zunehmende Nutzung von KI-generiertem Code birgt das Risiko, dass Sicherheitslücken und Fehler in kritische Infrastrukturen eingeschleust werden. Formale Verifikation kann diese Risiken mathematisch ausschließen, erfordert jedoch oft einen enormen manuellen Aufwand für das Schreiben logischer Annotationen (Spezifikationen, Invarianten, Beweisblöcke).

Bisherige KI-gestützte Verifikationsansätze konzentrierten sich hauptsächlich auf einzelne Funktionen oder einfache Algorithmen. Die Verifikation ganzer Datenstruktur-Module stellt jedoch eine deutlich höhere Herausforderung dar, da sie folgende Komplexitäten mit sich bringt:

• Mathematische Abstraktion: Es muss eine abstrakte mathematische Sicht (View) der Datenstruktur definiert werden, um logisch über deren Zustand zu reasoning.
• Typ-Invarianten: Es müssen Invarianten formuliert werden, die bei allen Operationen auf der Datenstruktur erhalten bleiben müssen.
• Kontextabhängigkeit: Verschiedene Methoden müssen gemeinsam unter einer geteilten Invariante verifiziert werden.
• Syntax- und Semantik-Hürden: Große Sprachmodelle (LLMs) haben oft Schwierigkeiten mit der spezifischen Syntax und den verifikationsspezifischen Semantiken von Verus (einer Verifikationserweiterung für Rust), z. B. der strikten Trennung zwischen ausführbaren Funktionen und reinen Spezifikationsfunktionen.

2. Methodik: Der VeriStruct-Ansatz

VeriStruct ist ein Framework, das LLMs nutzt, um Verifikationsannotationen für Rust-Datenstrukturen in Verus automatisch zu generieren und zu reparieren. Der Workflow besteht aus zwei Hauptphasen und mehreren spezialisierten Modulen:

A. Eingabe und Ziel

• Eingabe: Rust-Quellcode einer Datenstruktur (ohne Annotationen) und ein Satz von Unit-Tests, die das erwartete Verhalten beschreiben.
• Ziel: Ein vollständig annotierter Code, der vom Verus-Verifier erfolgreich verifiziert wird.

B. Phase 1: Generierung der Annotationen (GenAnnos)

Ein Planer-Modul analysiert den Code und entscheidet, welche der folgenden Module ausgeführt werden müssen (nicht alle sind für jede Aufgabe nötig):

1. View-Modul: Generiert eine mathematische Abstraktion (z. B. als Sequenz oder Menge), die die Implementierung von der Spezifikation entkoppelt.
2. Typ-Invarianten-Modul: Generiert logische Formeln, die für alle Instanzen der Datenstruktur gelten müssen (z. B. Bereichsprüfungen für Indizes).
3. Spezifikations-Modul: Generiert Vorbedingungen (requires), Nachbedingungen (ensures) und Spezifikationsfunktionen.
4. Beweis-Block-Modul: Generiert Beweisblöcke und Schleifeninvarianten, um dem Verifier zu helfen.

• Prompt-Engineering: Die Prompts enthalten detaillierte Verus-Syntax-Leitfäden, Schritt-für-Schritt-Anweisungen und Few-Shot-Beispiele, um Syntaxfehler zu minimieren.
• Verfeinerung (Refinement): Ein spezieller Schritt fordert das LLM auf, generierte Views zu überarbeiten, um sicherzustellen, dass sie abstrakt genug sind (Vermeidung von trivialen Kartesischen Produkten, die die Implementierungsdetails offenlegen).

C. Phase 2: Reparatur der Annotationen (RepairAnnos)

Da der erste Generierungslauf selten perfekt ist, führt VeriStruct eine iterative Reparatur-Schleife durch:

1. Der Verus-Verifier wird ausgeführt.
2. Bei Fehlern wird die Fehlermeldung analysiert.
3. Ein Reparatur-Modul wird basierend auf dem Fehlertyp ausgewählt (z. B. „Falsche Funktionsart in Annotation", „Verletzung von Vorbedingungen", „Testversagen").
4. Das LLM wird mit dem spezifischen Fehler und Reparatur-Anweisungen promptet, um den Code zu korrigieren.
5. Dieser Prozess wiederholt sich bis zur erfolgreichen Verifikation oder Erschöpfung des Iterationsbudgets.

3. Schlüsselbeiträge

1. Neuer Workflow für Datenstrukturen: Einführung eines LLM-gestützten Workflows, der über die Verifikation einzelner Funktionen hinausgeht und komplexe Datenstruktur-Module mit Views, Invarianten und multiplen Methoden adressiert.
2. Implementierung (VeriStruct): Ein funktionierendes Tool, das einen Planer, spezialisierte Generierungs- und Reparaturmodule sowie Syntax-Leitfäden integriert.
3. Umfassende Evaluation: Evaluation an 11 realistischen Rust-Datenstruktur-Benchmarks (u. a. Ringbuffer, Treemaps, Read-Write-Locks).

4. Ergebnisse

Die Evaluation wurde an 11 Benchmarks mit insgesamt 129 zu verifizierenden Funktionen durchgeführt:

• Erfolgsrate: VeriStruct verifizierte 10 von 11 Benchmarks erfolgreich.
• Funktionale Abdeckung: Es wurden 128 von 129 Funktionen (99,2 %) erfolgreich verifiziert.
• Vergleich mit Baselines:
  • Eine einfache Baseline (iteratives Anfordern ohne strukturierten Planer/Reparatur) schaffte nur 4/11 Benchmarks (52 Funktionen).
  • Claude Code (ein fortschrittlicher Agent) schaffte 8/11 Benchmarks (102 Funktionen), blieb aber hinter VeriStruct zurück.
• Effizienz: VeriStruct erreichte bessere Ergebnisse mit einem ähnlichen oder geringeren Token-Verbrauch als die Baseline, was die Effizienz des strukturierten Workflows unterstreicht.
• Besonderheit: Bei einem Benchmark (Bitmap) generierte das LLM eine Lösung, die fundamental anders (und einfacher) war als die menschliche Referenzlösung, indem es eine direktere Abstraktion wählte.

5. Bedeutung und Ausblick

VeriStruct stellt einen wichtigen Schritt hin zur skalierbaren, KI-gestützten formalen Verifikation dar. Es demonstriert, dass komplexe Datenstrukturen in Rust automatisiert verifiziert werden können, wenn man die KI durch strukturierte Planung, domänenspezifische Leitfäden und automatische Reparaturmechanismen führt.

Zukünftige Arbeiten umfassen:

• Integration von Retrieval-Augmented Generation (RAG) aus Verus-Bibliotheken.
• Unterstützung für Ressourcen-Algebra zur Verifikation komplexer paralleler Datenstrukturen.
• Automatisierte Generierung der Unit-Tests durch LLMs, um die manuelle Eingabe zu reduzieren.
• Anwendung von Reinforcement Learning, um die Suche nach optimalen Spezifikationen zu verbessern.

Zusammenfassend zeigt das Paper, dass die Kombination aus strukturiertem Workflow und modernen LLMs die Hürde für formale Verifikation senken und die Zuverlässigkeit von KI-generiertem Code signifikant erhöhen kann.