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

VeriStruct is een nieuw framework dat AI-assistentie uitbreidt naar het geautomatiseerde verifiëren van complexe datastructuurmodules in Verus door een planner te gebruiken voor het genereren van specificaties en een reparatiestap voor syntaxisfouten, wat resulteerde in een succesvolle verificatie van 99,2% van de geteste functies.

De kern

Stel je voor dat je een gigantische, complexe machine bouwt – bijvoorbeeld een robot die auto's repareert. Je wilt er 100% zeker van zijn dat deze robot nooit een fout maakt, geen bouten loslaat en geen mensen verwondt.

In de programmeerwereld noemen we dit verificatie: het wiskundig bewijzen dat code perfect werkt. Het probleem is dat dit normaal gesproken extreem moeilijk is. Het is alsof je elke schroef, elk tandwiel en elke stroomdraad in die robot met de hand moet controleren en een officieel certificaat moet schrijven. Dat kost jaren tijd en vereist supermenselijke expertise.

Nu komen er AI's (zoals de chatbots die je misschien kent) die kunnen programmeren. Dat is geweldig, want ze werken razendsnel. Maar ze maken ook fouten. Soms schrijven ze code die er goed uitziet, maar die in het echt crasht of veiligheidsrisico's bevat.

Hier komt VeriStruct om de hoek kijken. Het is een slimme "AI-assistent" die twee taken combineert:

1. Het laat een AI de code schrijven (of controleren).
2. Het laat een andere AI direct bewijzen dat die code veilig is, en repareert het direct als er een foutje in zit.

De Grote Uitdaging: Van Simpel naar Complex

Vroeger konden AI's alleen simpele taken bewijzen, zoals "een functie die twee getallen optelt". Maar echte software bestaat uit datastructuren – complexe verzamelingen zoals een rij wachtenden, een boom van bestanden of een ringbuffer (een soort draaiend opslagvakje).

Het bewijzen van deze complexe systemen is als het bewijzen van een heel gebouw, niet alleen één kamer. Je moet niet alleen kijken of de muren recht staan, maar ook of de fundering (de type invariant) stevig is en of de plattegrond (de abstractie) klopt.

Hoe werkt VeriStruct? (De Bouwmeester)

VeriStruct werkt als een super-georganiseerde bouwmeester met een team van gespecialiseerde AI's. Hier is hoe het proces eruit ziet, vertaald naar alledaagse termen:

1. De Plannera (De Chef)

Eerst kijkt de "Planner" naar de code en denkt na: "Wat hebben we hier nodig?"

• Moeten we een View maken? (Een abstracte tekening van hoe de data eruit ziet, zonder de rommelige details).
• Moeten we een Type Invariant maken? (Een regel die altijd waar moet zijn, zoals "de deur mag nooit open zijn als er iemand binnen is").
• Moeten we Specificaties schrijven? (Regels voor wat de code mag doen en wat het moet opleveren).

De Planner schakelt alleen de juiste AI's in. Hij wast geen auto als je alleen een band wilt vervangen. Dit bespaart tijd en voorkomt verwarring.

2. De Tekenaars (De Generatie)

De gespecialiseerde AI's gaan aan het werk. Ze proberen de wiskundige regels te schrijven die nodig zijn om de code te bewijzen.

• Het probleem: AI's zijn vaak niet goed in de specifieke taal van Verus (de taal waarin deze bewijzen worden geschreven). Ze gebruiken soms de verkeerde woorden of vergeten regels.
• De oplossing: VeriStruct geeft de AI's een "spiekbriefje" (prompt) met strikte regels en voorbeelden, zodat ze niet in de valkuilen lopen.

3. De Inspecteur en de Reparateur (De Reparaties)

Stel, de AI heeft een bewijs geschreven. De Verus-verifier (de strenge inspecteur) kijkt er naar en zegt: "Fout! Je hebt een verkeerde deur gebruikt."
In het verleden zou je dan alles moeten gooien en opnieuw beginnen. VeriStruct doet iets slimmers:

• Het pakt de fout op.
• Het stuurt het naar een Reparatie-module die precies weet hoe dit soort fouten op te lossen.
• De AI krijgt de foutmelding, leest de "spiekbriefjes" opnieuw en probeert het bewijs te repareren.

Dit proces (schrijven -> controleren -> repareren) herhaalt zich totdat de inspecteur tevreden is. Het is alsof je een puzzel legt, en als een stukje niet past, niet de hele puzzel weggooit, maar gewoon dat ene stukje vervangt tot het klopt.

Het Resultaat: Een Wonderbaarlijke Prestatie

De onderzoekers hebben VeriStruct getest op 11 complexe datastructuren (zoals een ringbuffer, een boomstructuur en een beveiligde slot).

• Zonder VeriStruct: Een simpele AI probeerde het. Hij slaagde er maar in om 4 van de 11 systemen te bewijzen.
• Met VeriStruct: Het systeem slaagde erin om 10 van de 11 systemen volledig te bewijzen.
• De cijfers: Van de 129 kleine onderdelen (functies) die bewezen moesten worden, lukte het om 128 te bewijzen (99,2%!).

Waarom is dit belangrijk?

Stel je voor dat we in de toekomst AI's gebruiken om de software te schrijven die onze ziekenhuizen, vliegtuigen of banken bestuurt. We kunnen niet zomaar hopen dat het goed gaat. We moeten het bewijzen.

VeriStruct toont aan dat we AI's niet alleen kunnen gebruiken om code te schrijven, maar ook om die code direct te verifiëren. Het maakt het mogelijk om grote, complexe bibliotheken met bewezen code te bouwen, zodat ontwikkelaars daarop kunnen bouwen zonder bang te hoeven zijn voor verborgen fouten.

Kortom: VeriStruct is de brug tussen de snelle, creatieve kracht van AI en de strenge, onverbiddelijke zekerheid van wiskundige bewijzen. Het zorgt ervoor dat we niet alleen sneller bouwen, maar ook veiliger.

Technische samenvatting

Probleemstelling

De opkomst van generatieve AI heeft de softwareontwikkeling versneld, maar introduceert ook risico's op bugs en kwetsbaarheden in kritieke digitale infrastructuur. Formele verificatie kan deze risico's mitigeren door wiskundig te bewijzen dat code correct is. Echter, de toepassing van formele verificatie in de praktijk wordt beperkt door de enorme inspanning en expertise die nodig is om complexe logische annotaties (specificaties, pre- en postcondities, invarianten) handmatig te schrijven.

Bestaande AI-gestuurde verificatiebenaderingen zijn tot nu toe beperkt tot het verifiëren van eenvoudige, tekstboekachtige algoritmen bestaande uit één enkele functie. Het verifiëren van volledige datastructuurmodules (zoals ringbuffers, bomen of locks) is aanzienlijk complexer omdat dit vereist:

1. Het definiëren van een wiskundige abstractie (view) van de datastructuur.
2. Het handhaven van type-invarianten die gelden voor alle operaties op de structuur.
3. Het gezamenlijk verifiëren van meerdere methoden onder een gedeelde invariant.

Daarnaast hebben Large Language Models (LLMs) moeite met de gespecialiseerde syntaxis en verificatie-semantiek van Verus (een verificatie-extensie voor Rust), wat leidt tot fouten in gegenereerde annotaties.

Methodologie: VeriStruct

De auteurs introduceren VeriStruct, een framework dat LLMs gebruikt om automatisch annotaties te genereren en te repareren voor Verus-datastructuren. Het systeem werkt met als input de Rust-broncode en een reeks eenheidstests, en produceert volledig verifieerbare code.

Het workflow bestaat uit twee hoofdfasen:

1. Generatiefase (Stage 1)

In plaats van alle annotaties in één keer te genereren, gebruikt VeriStruct een planner-module die bepaalt welke specifieke componenten nodig zijn voor de gegeven datastructuur. Het systeem bevat vier gespecialiseerde modules:

• View Module: Genereert een wiskundige abstractie (bijv. een reeks of verzameling) die de concrete implementatie vertaalt naar een logisch model.
• Type Invariant Module: Genereert logische formules die de geldige toestanden van de datastructuur beschrijven (bijv. indexgrenzen).
• Specificatie Module: Genereert requires (precondities) en ensures (postcondities) voor functies.
• Proof Block Module: Genereert bewijsblokken en loop-invarianten om de verifieerder te helpen.

De planner analyseert de code en selecteert alleen de noodzakelijke modules (bijv. een ringbuffer vereist een View, een invariant en specificaties). Voor elke module worden meerdere samples gegenereerd en de beste geselecteerd op basis van succesvolle verificatie.

2. Reparatiefase (Stage 2)

Omdat LLMs vaak fouten maken in Verus-syntaxis of semantiek (bijv. het aanroepen van uitvoerbare functies binnen specificaties), voert VeriStruct een iteratief reparatieproces uit:

• De gegenereerde code wordt verwerkt door de Verus-verifieerder.
• Bij fouten wordt het foutbericht geanalyseerd en gekoppeld aan een reparatiemodule (bijv. voor het corrigeren van typefouten, inconsistenties in mutabiliteit, of fouten in testasserties).
• De LLM wordt gevraagd de code te repareren op basis van het specifieke foutbericht en richtlijnen.
• Dit proces herhaalt zich tot de code verifieert of een maximum aantal iteraties is bereikt.

Om de kwaliteit te verhogen, bevat de prompt ook syntaxisrichtlijnen afgeleid van de Verus-documentatie en voorbeelden van correcte implementaties (in-context learning).

Belangrijkste Bijdragen

1. Nieuwe Workflow: Een LLM-gestuurde workflow die specifiek is ontworpen voor het verifiëren van complexe datastructuurmodules, in plaats van alleen losse functies.
2. Implementatie (VeriStruct): Een werkend systeem dat een planner, gespecialiseerde generatiemodules en een iteratief reparatiesysteem integreert.
3. Omgaan met LLM-beperkingen: Een hybride aanpak die syntaxisrichtlijnen in prompts integreert en een gespecialiseerde reparatiefase gebruikt om semantische en syntactische fouten automatisch te corrigeren.
4. Automatische Testgeneratie: Het paper merkt op dat het genereren van eenheidstests door LLMs wordt gebruikt om de belasting voor ontwikkelaars te verminderen, hoewel het systeem nog steeds een test-suite als input vereist.

Resultaten

Het framework is geëvalueerd op 11 Rust datastructuur-benchmarks (o.a. ringbuffers, bomen, locks) met in totaal 129 functies om te verifiëren.

• Succesratio: VeriStruct slaagde erin 10 van de 11 benchmarks volledig te verifiëren.
• Functie-dekking: Er werden 128 van de 129 functies (99,2%) succesvol geverifieerd.
• Vergelijking met Baselines:
  • Een eenvoudige baseline (LLM die herhaaldelijk code genereert zonder gestructureerde planner of reparatiemodules) slaagde slechts in 4 van de 11 benchmarks en verifieerde 52 functies.
  • Claude Code (een geavanceerde AI-agent) verifieerde 102 functies in 8 benchmarks, maar bleef achter bij VeriStruct, ondanks het gebruik van een nieuwere modelversie.
• Efficiëntie: VeriStruct bereikte betere resultaten met een vergelijkbaar of lager token-verbruik dan de concurrenten, dankzij de gestructureerde aanpak.

Betekenis en Toekomstperspectief

Dit paper markeert een belangrijke stap in de richting van schaalbare, AI-gestuurde formele verificatie. Het bewijst dat het mogelijk is om complexe, herbruikbare bibliotheken (datastructuren) automatisch te verifiëren, wat de basis legt voor het verifiëren van nog complexere systemen.

Toekomstig werk richt zich op:

• Integratie van Retrieval-Augmented Generation (RAG) om nuttige lemmata uit standaardbibliotheken op te halen.
• Ondersteuning voor concurrente datastructuren via resource algebra.
• Het gebruik van Reinforcement Learning (RL) om de zoekruimte voor specificaties en bewijzen efficiënter te verkennen.
• Volledige automatisering van het genereren van eenheidstests.

Kortom, VeriStruct verkleint de kloof tussen volledig handmatige formele verificatie en AI-assistentie, waardoor hogere automatisering wordt bereikt zonder in te leveren op de strenge eisen van correctheid.