LLM's maken formele softwareverificatie op veel grotere schaal mogelijk

Met behulp van Claude hebben we veiligheidseigenschappen bewezen op het niveau van assembly-code (RISC-V) in meer dan 100 echte open-source softwarebibliotheken. Voor zover wij weten, is dit de eerste grootschalige poging om AI te gebruiken om formele verificatie toe te passen op productiesoftware op assembly-niveau. Tijdens het schrijven van de bewijzen ontdekte Claude ook bugs die jarenlang onopgemerkt waren gebleven, ondanks biljoenen testruns. Naarmate de mogelijkheden van modellen blijven verbeteren, verwachten we dat formele verificatie een essentieel onderdeel wordt van veilige softwareontwikkeling.

Introductie

Zelfs volwassen, uitgebreid geteste software bevat bugs, en LLM's worden steeds vaker vaardig in het vinden ervan. De Linux-kernel—een van de best geteste stukken software van vandaag, ingezet op miljarden apparaten wereldwijd—had onlangs meer dan 1.000 openbaarde kwetsbaarheden. Omdat frontier-modellen steeds beter in staat zijn om schijnbaar onschuldige bugs te ketenen tot kritieke exploits, hebben we technieken nodig die deze bugs kunnen detecteren en herstellen voordat ze in het wild kunnen worden uitgebuit.

Ideaal gezien zouden dergelijke technieken alle bugs kunnen vinden en patchen, en vervolgens het bewijs kunnen leveren dat er geen meer te vinden zijn. Formele verificatie is een manier om dit te doen. Bij formele verificatie vertalen ontwikkelaars hun code naar een wiskundig model en proberen ze vervolgens te bewijzen dat deze altijd een gedefinieerde set veiligheidsregels volgt. Als het niet lukt om dit te bewijzen, betekent dit dat er een bug in de code kan zitten die een regel schendt; de aard van het falen geeft aan wat de bug zou kunnen zijn. Door dit proces te herhalen (en telkens de oorzaak van het falen te elimineren), levert dit uiteindelijk het bewijs op dat de code verstoken is van elke bug die die regels zou schenden.

Formele verificatie is echter niet eenvoudig. Bewijzen kunnen vele malen groter zijn dan de oorspronkelijke code, en het schrijven ervan vereist aanzienlijke inspanning en een niche, zeer gespecialiseerde set vaardigheden. Zo kostte het implementeren van de seL4-operating system kernel twee manjaren, maar het formeel verifiëren ervan kostte 20 manjaren. Bijgevolg was formele verificatie alleen praktisch in echt missie-kritieke toepassingen, zoals de avionica-code van Airbus.

Maar LLM's maken het veel gemakkelijker. Frontier-modellen kunnen nu volledig autonoom correctheidsbewijzen produceren voor real-world software. Om dit aan te tonen, hebben we Claude gevraagd om nuttige veiligheidseigenschappen te bewijzen voor 123 open-source bibliotheken, waaronder het aantonen dat sommige van hun uitvoerbare artefacten onder bepaalde omstandigheden nooit kunnen crashen. Specifiek bewees Claude dat deze programma's altijd normaal zullen afsluiten zonder geheugenfouten (memory-safety errors) of mislukte assertions te triggeren, voor elke input kleiner dan 64 MB en elke gemodelleerde Linux operating system (OS) respons en geheugenindeling, onder bepaalde aannames (namelijk dat het programma draait als een single-threaded statische binary met een vast geheugenbudget op een RISC-V CPU onder Linux OS). Dit is nog ver verwijderd van het oplossen van alle mogelijke bugs, maar het brengt ons veel dichterbij dan voorheen en biedt een roadmap naar dat doel.

We publiceren een subset van deze bewijzen zodat iedereen ze kan verifiëren en hergebruiken, samen met de RISC-V en OS-semantiek. Theorem, onze partner in dit project, biedt ook aan om dezelfde pipeline uit te voeren voor andere open-source projecten en publiceert een Claude-skill om ontwikkelaars te helpen bij het starten met het verifiëren van hun eigen code.

Formele verificatie is een breed veld met veel methodologieën. Hieronder beschrijven we ook onze eerste verkenningen met andere formele verificatiemethoden om andere beveiligings- of softwareontwikkelingstaken te versnellen, zoals het beoordelen van de veiligheid van het zlib-compressiealgoritme, het bewijzen van gedragsequivalentie van een Python-interpreter geschreven in Rust, en het uitroeien van langdurige bugs in kritieke software.

De weg vooruit voor formele verificatie is veelbelovend. De kosten voor het schrijven van bewijzen dalen naarmate modellen intelligenter worden. Bovendien, naarmate meer code wordt geformaliseerd en methoden voor het bereiken van veiligheidsgaranties meer gestandaardiseerd worden, zal het vermogen om bewijzen over codebases heen te hergebruiken of te wijzigen de kosten amortiseren. We moedigen alle ontwikkelaars aan om formele verificatie met LLM's te verkennen—vooral zij die het eerder hebben geprobeerd met minder capabele modellen en merkten dat het niet werkte.

Testen omzetten in bewijzen

Om te bewijzen dat een stuk software correct is, moeten we eerst vaststellen wat "correct" eigenlijk betekent. Correctheid wordt gedefinieerd door de specificatie (spec). In sommige programma's is er een duidelijke manier om het beoogde gedrag van het programma formeel te specificeren. Een PNG-decoder neemt bijvoorbeeld een reeks bytes en decodeert deze (volgens RFC 2083) naar de overeenkomstige afbeelding. Maar voor de meeste programma's is dit niet zo eenvoudig. Wat zou het betekenen voor een tekstverwerker of een webbrowser om "correct" te zijn? De moeilijkheid om een uitgebreide en ondubbelzinnige spec te verkrijgen is een aanzienlijk obstakel voor het verifiëren van software op grotere schaal.

Om dit aan te pakken voor de code in de open-source bibliotheken die we wilden bewijzen, hanteren we de aanpak om hun bestaande compileerbare testsuites automatisch om te zetten in een spec door de regel "deze testsuite slaagt altijd" te coderen, gebruikmakend van een algemeen model van wat het betekent om een willekeurige RISC-V-gecompileerde binary op Linux uit te voeren. Historisch gezien was het bewijzen van dergelijke specs onuitvoerbaar, gezien de inherente complexiteit van het schrijven van een bewijs dat alle mogelijke gedragingen en interacties van tienduizenden assembly-instructies over elke input kan omvatten (en het feit dat bewijzen als gevolg daarvan extreem groot neigen te zijn). Dit is waar huidige LLM's in beeld komen: het verwerken van miljoenen regels code met een goed gedefinieerd doel is een taak waar LLM's uiterst geschikt voor zijn.

Voor dit project begonnen we met fuzz-tests. In deze tests schrijven ontwikkelaars een entry point¹ in hun code die inputs accepteert, zodanig dat elke input die een crash veroorzaakt, een bug is waar de auteurs om geven. De fuzzer, een testengine, genereert vervolgens enorme aantallen semi-willekeurige en gemuteerde inputs bij het entry point om een bug te proberen te vinden. Hoe langer een fuzzer draait, hoe meer bugs hij kan vinden. Maar dit is inherent een brute-force proces, zonder garantie dat elk mogelijk codepad wordt doorlopen, ongeacht hoeveel inputs je probeert.

Om alle bugs te vinden die door een fuzz-test naar boven zouden zijn gebracht, zetten we de fuzz-test om in een spec gedefinieerd over de gecompileerde RISC-V-instructies. De spec stelt dat de fuzz-test niet zal crashen voor elke input kleiner dan 64 MB³. Als Claude deze spec kan bewijzen, wordt de fuzz-test op RISC-V overbodig: het fuzzen van dat entry point zal nooit bugs vinden.

We hebben dit gedaan voor honderden projecten in het OSS-Fuzz-initiatief van Google, dat continue fuzz-testing biedt voor kwalificerende open-source projecten. OSS-Fuzz bevat duizenden door ontwikkelaars geschreven entry points die zoeken naar defecte code-eigenschappen door te crashen (bijvoorbeeld bij een mislukte assertion). OSS-Fuzz instrumenteert C- en C++-programma's automatisch met AddressSanitizer (ASan)⁴, waardoor ze crashen zodra er onjuist toegang wordt gezocht tot het geheugen (een belangrijke oorzaak van softwarekwetsbaarheden). Breed spectrum specificaties zoals geheugensafety zijn van toepassing op bijna alle software.

Over een periode van enkele weken heeft Claude de gevonden bugs succesvol gepatcht en vervolgens bewezen dat er geen crashes optreden op elke input (tot 64 MB) voor 239 entry points verspreid over 123 verschillende OSS-Fuzz-bibliotheken. Deze bewijzen opereren op de gecompileerde RISC-V-instructies (d.w.z. executable binaries) en bestaan uit ongeveer 180 miljoen regels Rocq; een typisch bewijs loopt op tot ongeveer 600.000 regels om veiligheidsgaranties te bieden voor binaries met een mediane lengte van 18.000 RISC-V-instructies. Deze bewijzen zijn gebouwd door de RISC-V assembly-code te vertalen naar een wiskundig model met behulp van de RISC-V-instructie- en Linux-processemantiek van Theorem. Dit betekent dat deze bewijzen momenteel aannemen dat het programma draait als een single-threaded statische binary met een vast geheugenbudget op een RISC-V CPU onder Linux OS. Het uitbreiden van de scope van deze bewijzen is goed haalbaar, aangezien dit het standaardiseren van semantiek voor meer assembly-architecturen en andere besturingssysteemprocessen zou inhouden.

Hoewel dit een enorm volume aan bewijscode is, hoeft er vrijwel niets handmatig te worden beoordeeld. De Rocq-bewijschecker garandeert dat de spec correct wordt voldaan door het bewijs. Als resultaat zijn de enige artefacten die een ontwikkelaar moet vertrouwen:

• De formele modellen van RISC-V en van Linux-processen;
• De exacte stellingen (theorems) die zijn bewezen;
• De Rocq-bewijschecker zelf⁵.

Dit betekent niet dat deze bibliotheken geen bugs bevatten. In plaats daarvan betekent het dat eventuele resterende bugs zich ofwel bevinden in de bovenstaande artefacten, ofwel buiten de scope van het bewijs van Claude vallen. Het versterken van die mogelijk nog bug-gevoelige vertrouwde componenten (Rocq, RISC-V en Linux-semantiek) is niet onbetekenend, maar het is een veel hanteerbaardere taak dan het debuggen van elke regel code die de opgeschaalde bewijzen bestrijken—vooral omdat deze aanpak een willekeurig aantal projecten kan beveiligen zonder de omvang van de vertrouwde componenten te vergroten.

Bugs vinden en herstellen

Bovenstaand hebben we laten zien dat je veel door ontwikkelaars geschreven tests (fuzz-tests) van open-source bibliotheken kunt omzetten in specs die Claude kan bewijzen dat altijd zullen slagen, soms nadat de resterende gevonden bugs zijn gepatcht. Om deze reden heeft het proces van het proberen te bewijzen van deze specs honderden bugs blootgelegd.

Tijdens de pogingen van Claude om honderden entry points te bewijzen, kwamen veel bugs naar voren. Om te voorkomen dat Claude telkens moest stoppen voor een mens, lieten we Claude de bugs die hij vond zelf herstellen: hij patchte de code, waardoor de spec opnieuw werd gegenereerd met die gepatchte code, waarna Claude verderging met het bewijzen van die nieuwe spec⁶.

Veel van de gevonden bugs zijn zodanig dat een fuzzer ze waarschijnlijk nooit zou vinden. Fuzzers muteren kleine inputs, meestal begrensd op 1 MB, en vertrouwen doorgaans op code-coverage om hen naar bugs te leiden. Tijdens het bewijzen van een entry point in een bibliotheek vond Claude een counter underflow in een decompressor die leidde tot een out-of-bounds write, maar alleen bij inputs van ongeveer 20 MB met een zeldzame, specifieke lay-out. Andere bugs omvatten een out-of-bounds read in een image-decoder die een input van 64 MB en meer dan 2 GB geheugen nodig had, een out-of-bounds read in een andere bibliotheek die een specifieke volgorde van aanroepen over twee handles naar hetzelfde bestand vereiste, en een herontdekking van CVE-2026-56132 in libexpat, die diep geneste input nodig had. Claude vond ook logische bugs die helemaal niet crashen. Tijdens het bewijzen dat een bibliotheek geheugenveilig was, merkte hij bijvoorbeeld op dat een functie om te beperken welke bestanden een applicatie kan laden, niet altijd wordt afgedwongen.

Het uiteindelijke doel van dit project was om een bewijs te leveren dat de RISC-V-gecompileerde fuzz-tests geen resterende crashes bevatten. Echter, bugs zoals hierboven beschreven tonen aan dat het proces nog een ander voordeel heeft, ongeacht of dat doel wordt behaald: zelfs alleen al het proberen van dit proces levert echte bugs op die hersteld moeten worden.

Meer bewijzen dan alleen geheugenveiligheid

Het bewijzen dat een fuzz-test geen crashes meer bevat, is significanter dan het klinkt. Het is gebruikelijk dat fuzz-tests in real-world code testen op schendingen van betekenisvolle high-level eigenschappen, zoals encode-decode roundtripping, idempotentie, algebraïsche wetten, differentiële testen, zelfconsistentie of equivalentie met referentie-implementaties. Een fuzz-test voor het LZO-compressiealgoritme stelt bijvoorbeeld dat als je een input comprimeert en vervolgens decomprimeert, het resultaat hetzelfde is als het origineel. Als deze eigenschap niet geldt, crasht het programma—het bewijzen dat de test nooit crasht is dus equivalent aan het bewijzen van de eigenschap zelf.

Dit kan ook gebeuren wanneer de eigenschappen niet direct door de ontwikkelaar zijn gespecificeerd. Om bijvoorbeeld het OSS-Fuzz-bewijs voor cpp-httplib te voltooien, was het noodzakelijk om de mogelijkheid van een stack overflow door te veel recursie in de std::set destructor uit te sluiten. Deze recursiediepte is begrensd door de maximale diepte van een boom, dus Claude moest (op machinecode-niveau!) bewijzen dat het red-black tree rebalancing-algoritme van libc++ correct is geoptimaliseerd om de diepte van de boom logaritmisch begrensd te houden.

Andere casestudies van formele verificatie

Formele verificatie is een uitgebreid domein. Het voorbeeld van fuzz-test-naar-bewijs is één instantie van hoe LLM's formele verificatie breder bruikbaar maken door bewijzen direct toe te passen op machinecode.

We hebben ook succes behaald door LLM's op andere manieren met formele verificatie te gebruiken. Zo hebben we Claude gevraagd om een formele spec te schrijven van RFC 1950, het technische document dat het zlib-compressiebestandsformaat definieert. Vervolgens lieten we Claude bewijzen dat de zlib-implementatie in de Linux-kernel die spec correct implementeert. Net als bij de voorgaande voorbeelden bewees Claude deze eigenschap op binair niveau, maar in plaats van RISC-V bewees Claude direct de x86-gecompileerde binary met behulp van door Claude gegenereerde (en zwaar geteste) formele semantiek van de x86 ISA⁷. We herhaalden dit proces voor een half dozijn andere veelgebruikte bibliotheken. Onderweg vonden we enkele kleine (niet uitbuitbare) bugs in randgevallen, die momenteel worden gemeld bij de upstream-ontwikkelaars. We trekken hieruit twee conclusies: (1) deze extreem goed geteste codebases zijn al bijna volledig correct, en (2) het is mogelijk om end-to-end correctheidseigenschappen te bewijzen over bestaande real-world codebases.

In een ander experiment hebben we Claude gevraagd om een interpreter voor een groot deel van Python in Rust te ontwikkelen, en te bewijzen (met behulp van Verus, een verificatietool voor Rust) dat deze voldoet aan de CPython-semantiek zoals beschreven in een academisch paper. We hebben de naleving van het CPython-gedrag vervolgens empirisch gemeten door meer dan 1,7 miljoen willekeurig gegenereerde Python-programma's te draaien, waarbij we in 99,95% van de tests identiek gedrag vonden met CPython; de resterende verschillen waren begrijpelijke bekende randgevallen.

We vonden ook problemen in verschillende veelgebruikte en kritieke applicaties via pogingen tot formele verificatie van eenvoudige veiligheidseigenschappen. In één daarvan ontdekten we een voorheen onbekende logische bug die meer dan een decennium latent was gebleven. Tijdens een poging om een veelgebruikte PDF-lezer te verifiëren, vonden we in één week net zoveel beveiligingsbugs als er doorgaans in een jaar worden gemeld.

Dit is pas het begin

Een van de belangrijkste beperkingen van LLM-ondersteunde formele verificatie is dat de bewijzen honderden miljoenen tokens kunnen kosten om te produceren. Kostenefficiëntie is cruciaal als we deze methoden beschikbaar willen maken voor het gehele software-ecosysteem. Gelukkig zijn er dwingende redenen om te verwachten dat de efficiëntie zal verbeteren.

Nieuwere modellen hebben minder tokens nodig

We hebben 36 kleine verificatietaken gebouwd uit echte OSS-Fuzz code. Opus 5.5 bewijst de helft daarvan met ongeveer 40% minder tokens dan Opus 5. We verwachten dat deze trend zich voortzet naarmate modellen worden getraind op lange verificatietaken.

Bewijzen kunnen worden hergebruikt

Wanneer agenten afzonderlijk werken, dupliceren ze vaak veel inspanning. Bewijzen worden, net als software, recursief opgebouwd uit kleinere bewijzen—en hoe kleiner de bewijzen zijn, hoe herbruikbaarder ze neigen te zijn. Om de impact hiervan te meten, lieten we agenten elkaars bewijzen kopiëren terwijl ze werkten aan hun eigen doelen. Met toegang tot deze gedeelde workspace hadden agenten 17% minder tokens nodig dan wanneer ze alleen werkten, en sommige agenten slaagden zelfs nadat ze eerder in een solo-poging waren gefaald.

We observeerden hetzelfde fenomeen op schaal tijdens onze OSS-Fuzz-bewijzingsinspanning. Het grootste deel van een bewijs betreft code die elk programma bevat (met name de initialisatie van de C-runtime en AddressSanitizer), waardoor zeer verschillende programma's kunnen eindigen met aanzienlijk overlappende bewijzen. Agent-teams maakten hiervan gebruik door het voltooide bewijs van een ander team te kopiëren en dit vervolgens aan te passen aan hun eigen programma.

Deze herbruikbaarheid van bewijzen is hoe Mathlib, een gedeelde bibliotheek van formele wiskunde in Lean, is gegroeid naar bijna 300.000 theorema's ingediend door meer dan 700 bijdragers: elk nieuw bewijs bouwt voort op het bestaande werk. We hebben een vergelijkbare verzameling bewijzen opgebouwd tijdens onze OSS-Fuzz-inspanning, waarvan we er enkele opnemen in onze release (we publiceren geen bewijzen die een niet-gepatchte bug in de open-source software kunnen onthullen).

Nu we deze eerste experimenten afronden, hebben we een strategie nodig voor het verifiëren van de enorme hoeveelheid bestaande software, beginnend bij de meest kritieke afhankelijkheden. Zoals we hebben laten zien, kan dit op schaal worden bereikt door generieke specs te gebruiken en op binair niveau te werken, waardoor de noodzaak om volledige codebases in een andere taal te herschrijven wordt omzeild.

Deze aanpak vergemakkelijkt ook het hergebruik van bewijzen op pakketniveau, wat betekent dat elke afhankelijkheid slechts één keer geverifieerd hoeft te worden. Afhankelijkheden volgen een machtswet: het bewijzen van zelfs een kleine set gedeelde bibliotheken maakt het haalbaar om een enorme hoeveelheid software te bewijzen.

Beperkingen

In de praktijk kan formele verificatie soms minder bewijzen over de veiligheid van de code dan we zouden willen.

"Formeel geverifieerd" betekent niet "bug-vrij." Claude kan een bewijs schrijven dat aantoont dat het gedrag van een gecompileerd programma voldoet aan de vereisten van een formele spec (die wordt geverifieerd door een externe bewijschecker). Een bewijschecker kan echter niet vertellen of je spec overeenstemt met de realiteit. Om overeen te stemmen met de realiteit, moet de spec correct alles omvatten en modelleren over de real-world machine waarop het geverifieerde programma draait, inclusief de CPU en het besturingssysteem. Wanneer bugs verschijnen in geverifieerde code, komt dat omdat de spec, of de aangenomen semantiek van de machine, afwijkt van de realiteit.

Hieronder staan de manieren waarop dit van toepassing is op onze bewijzen, en ideeën voor toekomstig werk om die gaten te dichten:

• De echte machine doet iets wat het model niet beschrijft. Onze bewijzen gaan over single-threaded, statische RISC-V binaries gelinkt tegen musl libc. De meeste mensen draaien deze bibliotheken echter op x86 of ARM en linken ze dynamisch tegen glibc. Om dit gat te dichten, hebben we systeemmodellen nodig die nauwer aansluiten bij ingezette systemen. Een stap hiervoor zou het genereren van nauwkeurige semantiek voor x86 zijn.
• De claim is mogelijk niet allesomvattend. We hebben bewezen dat er geen crash optreedt voor elke input onder de 64 MB op veel fuzzing entry points in Google OSS-Fuzz, inclusief ASan-crashes. ASan detecteert echter niet alle geheugenveiligheidsbugs, en we hebben niet alle entry points voor elke bibliotheek geverifieerd. Zelfs als we dat hadden gedaan, zou de hele bibliotheek niet gedekt zijn door het verifiëren van alle entry points (vooral als er dead code is). Daarnaast kunnen echte programma's de bibliotheek verkeerd gebruiken, wat leidt tot geheugencorruptie in de aanroeper. Om dat gat te dichten, zouden we moeten specificeren wat aanroepers moeten doen voor elke publieke functie, en aanroepers zouden zich hier strikt aan moeten houden.

We verwachten dat naarmate we meer leren over het inzetten van LLM's voor formele methoden, en naarmate modellen blijven verbeteren, deze beperkingen hanteerbaar worden en we een veel groter percentage van de code kunnen verifiëren waar we op vertrouwen.

Conclusie

De trend is duidelijk: formele verificatie, die historisch gezien alleen praktisch was voor op maat gemaakte expert-garanties in de meest veiligheidskritieke code, zal binnenkort net zo praktisch zijn als fuzzing vandaag de dag is voor bijna alle productiesoftware. Net als statische types, testframeworks en andere correctheidstools, zal verificatie rijpen van "achteraf toegevoegd" naar "ingebouwd," gedreven niet alleen door LLM's, maar ook door innovaties in taalontwerp en ontwikkelingsworkflows.

In de wereld van vandaag—waar LLM's automatisch scannen naar en steeds meer code-kwetsbaarheden vinden—moeten we processen gebruiken die code-veiligheidseigenschappen kunnen garanderen. Op LLM-schaal is formele verificatie een veelbelovende aanpak om deze garanties te beveiligen op een scope en schaal die voorheen onbereikbaar waren. We moedigen anderen aan om te experimenteren, zodat we collectief een wereld kunnen bouwen waarin robuuste software wijdverspreid is en softwarebugs een goed begrepen en snel oplosbare zeldzaamheid zijn.

***

Voetnoten

¹ RISC-V is een processorontwerp, zoals x86 of ARM, dat de assembly-instructies (de basiscommando's die een chip uitvoert) definieert waar software naar wordt gecompileerd.

² Een entry point is een "voordeur" naar de code, ter beschikking gesteld door de auteurs voor testen. Elke input bij het entry point die een crash veroorzaakt, is een bug waar de auteurs om geven.

³ Het verhogen hiervan vereist een triviale menselijke inspanning om de parameter te wijzigen en de spec opnieuw te genereren, waarna Claude de stelling opnieuw bewijst.

⁴ AddressSanitizer (ASan) is een compiler-tool die controles toevoegt aan een programma, zodat geheugenfouten, zoals buffer overflows en use-after-free, worden gedetecteerd en gemeld op het moment dat ze tijdens runtime optreden.

⁵ Dit betekent technisch gezien ook dat we de hardware, het OS en de OCaml-compiler moeten vertrouwen waarop de Rocq-bewijschecker vertrouwt.

⁶ Let op dat dit de deur openzet voor reward hacking. Reward hacking is wanneer een AI-model een shortcut vindt die technisch voldoet aan het gestelde doel zonder te doen wat eigenlijk bedoeld was. In deze context zou Claude elk theorema bewijsbaar kunnen maken door het programma te herschrijven naar een programma dat triviaal nooit crasht. Om dit te ontmoedigen, hebben we elke patch bestraft en extra credits aangeboden voor het bewijzen welke inputs worden gewijzigd en hoe weinig deze zijn. We hebben de patches ook gelogd en gecontroleerd op deze foutmodi.

⁷ We denken dat het vermogen van Claude om—volledig autonoom—de formele semantiek van een ISA te genereren een aparte, interessante les is. Hoewel we niet zeker kunnen zijn dat onze semantiek zelf perfect is, hebben we empirisch vastgesteld dat het stapsgewijs doorlopen van onze semantiek een Ubuntu userspace kan booten bovenop een Linux-kernel. Het genereren van deze semantiek identificeerde ook honderden fouten in de officiële referentiedocumentatie, samen met een kleiner aantal bugs in de hardware zelf.