Stel je voor dat je een huis bouwt met een set magische, zelfcorrigerende stenen. Deze stenen, genaamd "Rust", staan bekend omdat ze een ingebouwde veiligheidsinspecteur hebben die weigert iets instabiels te laten bouwen. Als je een raam probeert te plaatsen waar een muur zou moeten zitten, schreeuwt de inspecteur "Nee!" en stopt hij je nog voordat je de eerste steen hebt gelegd. Dit maakt Rust ongelooflijk veilig voor het bouwen van software, omdat het crashes en beveiligingslekken voorkomt voordat ze plaatsvinden. Maar soms moet een meesterbouwer iets doen wat de inspecteur niet begrijpt — zoals het gebruik van een speciaal, gevaarlijk gereedschap om een zware balk snel te verplaatsen. In de wereld van Rust wordt dit "unsafe code" genoemd. Het is als een geheim pasje waarmee je de inspecteur kunt omzeilen, maar het komt met een zware prijs: als je één fout maakt, kan het hele huis instorten. Om het huis overeind te houden, moet je een zeer strikt, wiskundig "regelboek" (een specificatie) schrijven dat precies bewijst hoe je deze gevaarlijke gereedschappen veilig gebruikt. Maar het handmatig schrijven van deze regelboeken is ontzettend moeilijk, traag en gevoelig voor menselijke fouten.

Hier begint het verhaal van KaPilot. De onderzoekers achter dit project stelden een simpele vraag: kunnen we een superintelligent computerbrein (een AI) leren om deze veiligheidsregelboeken voor ons te schrijven? De uitdaging is dat deze AI's geweldig zijn in het schrijven van code, maar ze kopiëren vaak de fouten in de code die ze zien, in plaats van de intentie erachter te begrijpen. Ze kunnen een regelboek schrijven dat er perfect uitziet, maar een minuscuul, dodelijk detail mist. Het papier presenteert KaPilot, een team van AI-agenten die samenwerken om dit puzzelstukje op te lossen. In plaats van de AI alleen te vragen om "een regel te schrijven", gedraagt KaPilot zich als een detective, een schrijver en een strikte redacteur, allemaal tegelijk. Het leest de aantekeningen van de bouwer (documentatie), extraheert de echte veiligheidsregels, schrijft een concept, controleert het op gaten en voert het vervolgens door een rigoureuze test om te controleren of het daadwerkelijk werkt. Het resultaat is een systeem dat automatisch hoogwaardige veiligheidsregels kan genereren voor gevaarlijke code, waardoor het veel gemakkelijker wordt om veilige software te bouwen zonder dat er een team van menselijke experts nodig is om elke regel handmatig te schrijven.

De Detective, de Schrijver en de Redacteur

Denk aan het proces van het verifiëren van unsafe Rust-code als het schrijven van een perfecte instructiehandleiding voor een snelle racewagen die geen remmen heeft. Als de handleiding fout is, crasht de auto. Als de handleiding te vaag is, weet de bestuurder niet hoe hij moet rijden. Als de handleiding te streng is, kan de bestuurder helemaal niet bewegen.

KaPilot is een multi-agent framework, wat gewoon een chique manier is om te zeggen dat het een team van gespecialiseerde AI-personages is die samenwerken. Hier is hoe zij hun rollen spelen:

1. De Detective (SafetyReq): Voordat er iets geschreven wordt, moet het team weten wat de regels zouden moeten zijn. Meestal zijn deze regels verborgen in de rommelige, door mensen geschreven aantekeningen (documentatie) die bij de code horen. De "SafetyReq"-agent fungeert als een detective. Het leest deze aantekeningen, negeert de franje en extraheert een schone, beknopte lijst van veiligheidseisen. Het is als het omzetten van een warrig verhaal over "raak de rode knop niet aan" naar een duidelijke, genummerde lijst: "1. Druk niet op de rode knop. 2. Sta niet binnen 5 voet van de rode knop." Deze stap is cruciaal omdat het voorkomt dat de AI simpelweg de fouten in de code kopieert.
2. De Schrijver (SpecGenerate): Zodra de detective de lijst heeft, stapt de "SpecGenerate"-agent in. Het is de schrijver die die lijst omzet in een formele, wiskundige taal die de computer kan begrijpen (specifiek een taal genaamd Kani). De schrijver gokt niet zomaar; het gebruikt de lijst van de detective als een strikte gids.
3. De Redacteur (SpecPrecheck): Voordat het concept van de schrijver naar de eindbaas gaat, beoordeelt de "SpecPrecheck"-agent het. Het is een strikte redacteur die vraagt: "Heb je elk punt behandeld dat de detective vond? Is je zin te zwak? Is hij te sterk?" Als het concept slordig is, stuurt de redacteur het met specifieke opmerkingen over hoe het te verbeteren terug naar de schrijver. Dit gebeurt in een lus totdat het concept solide is.
4. De Testchauffeur (SpecVerify): Ten slotte neemt de "SpecVerify"-agent het concept en onderwerpt het aan een realiteitstest. Het gebruikt een tool genaamd Kani om miljoens verschillende riagementscenario's te simuleren om te zien of de auto crasht. Als de auto crasht (de verificatie mislukt), vertelt de Testchauffeur de Schrijver precies waarom de auto crashte, en begint de lus opnieuw.

De "Shuffle and Mix" Strategie

Hier worden de makers van het team echt slim. Soms genereert de AI een paar verschillende versies van het regelboek. Eén versie heeft misschien een perfecte "startvoorwaarde" (precondition) maar een zwakke "eindvoorwaarde" (postcondition). Een andere versie heeft misschien een zwakke start maar een perfect einde. Als je er gewoon één zou kiezen, mis je misschien de beste combinatie.

KaPilot gebruikt een strategie genaamd "shuffle-and-implication." Stel je voor dat je een kaartspel hebt, waarbij elke kaart een ander deel van het regelboek is. Het team schudt deze kaarten door elkaar en mengt de beste "start" van de ene versie met de beste "end" van een andere. Vervolgens testen ze deze nieuwe combinaties om te zien of ze zelfs nog beter werken dan de oorspronkelijke concepten. Het is alsof je de beste motor uit de ene auto en de beste banden uit een andere auto neemt om de ultieme racewagen te bouwen. Dit zorgt ervoor dat ze niet genoegen nemen met een "goed genoeg" regelboek, maar de best mogelijke versie vinden.

Wat ze vonden

De onderzoekers testten KaPilot op 124 verschillende stukjes unsafe Rust-code. Ze verdeelden deze in twee groepen:

• De Gold Set (54 functies): Deze hadden "ground truth" regelboeken geschreven door menselijke experts, zodat het team kon controleren of het werk van KaPilot correct was.
• De Ultra Set (70 functies): Deze hadden geen menselijke regelboeken, dus controleerde het team alleen of KaPilot enig werkend regelboek kon genereren.

De resultaten waren indrukwekkend. Voor de Gold Set genereerde KaPilot succesvol een werkend regelboek voor 88,9% van de functies. Nog belangrijker is dat het in 57,4% van de gevallen een regelboek schreef dat net zo goed of zelfs beter was dan het exemplaar van de menselijke experts. Voor de Ultra Set slaagde het erin om werkende regelboeken te maken voor 71,4% van de functies.

Toen ze KaPilot vergeleken met een andere AI-tool genaamd AutoSpec (die werd aangepast om met dit nieuwe systeem te werken), won KaPilot met gemak. Het produceerde 14,8% meer regelboeken die de tests daadwerkelijk doorstonden, en 25,9% meer regelboeken die semantisch gelijkwaardig aan of beter dan de door mensen geschreven versies waren.

Waarom dit ertoe doet

Het artikel betoogt dat het simpelweg vragen aan een AI om "een veiligheidsregel te schrijven op basis van deze code" niet goed werkt. De AI heeft de neiging om de fouten in de code te kopiëren of raakt in de war door de complexiteit. Door de taak op te splitsen in een team van specialisten — één om de aantekeningen te lezen, één om te schrijven, één om te redigeren en één om te testen — vermijdt KaPilot deze valkuilen.

De onderzoekers ontdekten ook dat de kwaliteit van de menselijke aantekeningen (documentatie) veel uitmaakt. Als de aantekeningen vaag zijn, heeft de AI het moeilijk. Maar wanneer de aantekeningen duidelijk zijn, blinkt KaPilot uit. Ze ontdekten ook dat hun "shuffle"-strategie een sleutelcomponent was; zonder deze strategie zou het systeem vaak genoegen nemen met een middelmatige oplossing in plaats van de perfecte combinatie van regels te vinden.

Kortom, KaPilot suggereert dat we niet hoeven te kiezen tussen menselijke expertise en AI-snelheid. Door AI te gebruiken als een team van gespecialiseerde assistenten die een strikt, logisch proces volgen, kunnen we de creatie van veiligheidsregels voor de gevaarlijkste delen van onze software automatiseren, wat de digitale wereld een veiligere plek maakt. Het artikel beweert niet dat dit elk probleem oplost (sommige complexe lussen hebben nog steeds menselijke hulp nodig), maar het bewijst dat deze multi-agent benadering een enorme stap voorwaarts is in het automatiseren en betrouwbaar maken van softwareverificatie.