Je hoeft de AI niet op haar woord te geloven: Claude levert bij software een wiskundig bewijs
Hoe weet je of werk van een AI deugt als niemand het kan nalezen? Anthropic laat Claude een wiskundig bewijs meeleveren dat een klein programma stap voor stap controleert. Zo onderzocht Claude 123 veelgebruikte softwarebouwstenen en vond honderden verborgen fouten.
AI schrijft een steeds groter deel van alle software, en ook steeds vaker de controle daarop. Dat roept een lastige vraag op: hoe weet je dat het klopt, als niemand het werk nog helemaal kan nalezen? Anthropic liet op 22 oktober 2026 een antwoord zien. De AI levert niet alleen het werk, maar ook een bewijs dat het werk doet wat het moet doen, en een klein, betrouwbaar programma controleert dat bewijs. Je hoeft de AI dan niet op haar woord te geloven.
Anthropic deed dit samen met Theorem, een bedrijf dat software wiskundig controleert. Ze lieten AI-model Claude 123 veelgebruikte open-sourcebibliotheken onderzoeken: gratis bouwstenen die in talloze apps, websites en servers zitten, bijvoorbeeld om bestanden in te pakken of afbeeldingen te tonen. Claude bewees dat ze niet vastlopen, en vond onderweg honderden fouten die jaren verborgen waren gebleven.
Een bewijs in plaats van een belofte
Vraag je een AI-assistent nu om code te controleren, dan krijg je een antwoord als "ik heb het nagekeken, het klopt". Of dat waar is, moet je zelf uitzoeken. Hier gaat het anders. Claude schrijft een volledige wiskundige uitwerking waarom de code bij elke invoer goed gaat, net zoals een leerling bij een wiskundetoets elke stap opschrijft.
Die uitwerkingen zijn enorm: een typisch bewijs telt ongeveer 600.000 regels. Geen mens leest dat. Dat hoeft ook niet, want een klein controleprogramma, Rocq, rekent elke stap na, zoals een leraar die een uitwerking regel voor regel nakijkt. Klopt er één stap niet, dan wordt het hele bewijs afgekeurd. Wie het resultaat wil vertrouwen, hoeft dus alleen dat controleprogramma te vertrouwen, plus de precieze afspraak over wat er bewezen moest worden. Dit heet formele verificatie.
Rocq is zelf geen AI. Het Franse onderzoeksinstituut Inria begon er in 1984 aan, en in 1989 verscheen de eerste versie, toen nog onder de naam Coq. Wiskundigen en informatici vertrouwen er al tientallen jaren op. Zo werd er in 2002 het bewijs mee gecontroleerd van de beroemde vierkleurenstelling: elke landkaart is met vier kleuren in te kleuren zonder dat buurlanden dezelfde kleur krijgen.
Deze aanpak werkt ook voor code die Claude zelf schrijft. Vond Claude een fout, dan repareerde het die en bewees het daarna dat de nieuwe versie wel goed werkt. Om valsspelen te voorkomen, bijvoorbeeld een programma ombouwen tot iets dat niets meer doet en dus ook nooit vastloopt, kregen reparaties strafpunten en controleerde het team ze achteraf. In een aparte proef schreef Claude zelf een programma dat een groot deel van de programmeertaal Python kan uitvoeren, en bewees het dat dit zich gedraagt zoals de officiële versie.
Gewone tests missen veel
Software wordt normaal getest door haar te bestoken met willekeurige invoer, zoals een kind dat op alle knoppen tegelijk drukt. Google doet dat voor veel open-sourceprojecten dag en nacht. Maar een test ziet alleen wat er misgaat bij de invoer die toevallig is geprobeerd. Een bewijs dekt alle invoer, in dit geval elk bestand tot 64 megabyte.
Dat verschil was meteen te merken. Volgens Anthropic vond Claude in een paar weken honderden fouten die ondanks biljoenen testrondes jaren onopgemerkt waren gebleven. Veel ervan zijn geheugenfouten, waarbij een programma buiten zijn eigen stukje geheugen schrijft of leest. Zulke fouten kunnen aanvallers soms gebruiken om een computer over te nemen. Een paar voorbeelden:
- Een programma dat ingepakte bestanden uitpakt, ging alleen de mist in bij een bestand van ongeveer 20 megabyte met één zeldzame opbouw.
- Een programma dat afbeeldingen inleest, faalde pas bij een bestand van 64 megabyte en meer dan 2 gigabyte werkgeheugen. Zo groot maken tests het zelden.
- Een functie die moet beperken welke bestanden een app mag openen, deed dat niet altijd. Er liep niets vast, dus geen test merkte het op.
- Claude vond zelfstandig een bekend lek terug in libexpat, een veelgebruikte bouwsteen die XML-bestanden leest. Dat lek is dit jaar gedicht.
Bij een programma dat pdf-bestanden leest, vond het team in één week evenveel beveiligingsfouten als er normaal in een heel jaar worden gemeld. In een ander belangrijk programma zat een denkfout die al meer dan tien jaar onopgemerkt was.
Wat het bewijs wel en niet zegt
Wiskundig bewezen betekent niet foutloos, benadrukken de onderzoekers zelf. Het bewijs geldt precies voor wat er is afgesproken: het programma loopt niet vast. Een fout waarbij niets vastloopt, valt erbuiten.
De bewijzen gelden ook voor een vereenvoudigde situatie: programma's die één taak tegelijk doen, op processors van het type RISC-V, een open ontwerp dat vrij te gebruiken is. De meeste laptops en telefoons gebruiken een ander type. De volgende stappen zijn die gangbare processors en programma's die meerdere taken tegelijk uitvoeren.
En het is nog duur: één bewijs kan honderden miljoenen tokens kosten, de stukjes tekst waarin een taalmodel werkt. Dat daalt snel. In een proef had Claude Opus 5.5 ongeveer 40 procent minder rekenwerk nodig dan het vorige model, Opus 5.
Anthropic en Theorem zetten een deel van de bewijzen openbaar online, zodat anderen ze zelf kunnen nalopen. Bewijzen die nog niet gedichte lekken zouden verraden, houden ze voorlopig achter. Theorem biedt open-sourceprojecten aan om hun code op dezelfde manier te laten controleren.
Wat betekent dit voor de weg naar de singulariteit?
Hoe sneller AI werkt, hoe groter het probleem van nakijken wordt. Mensen kunnen niet alles lezen wat een AI in een paar weken maakt, en dat remt hoeveel werk we aan AI durven over te laten. Een bewijs dat een machine kan nakijken, haalt die rem weg: het vertrouwen zit dan niet meer in de AI zelf, maar in een klein programma dat iedereen kan controleren.
Werk dat vroeger jaren menselijke inspanning per project kon kosten, deed Claude hier voor 123 bibliotheken samen in een paar weken. Als bewijzen goedkoper worden en ook voor gewone computers gaan gelden, kan AI straks belangrijke software bouwen én aantonen dat die deugt. Dat is een stevig fundament voor een wereld waarin AI steeds meer van het werk doet.
