Amazon investeert in wiskundig bewijs voor veilige AI-agents

TL;DR

• Wat: Amazon doet de grootste investering ooit in de Lean Focused Research Organization, een onafhankelijke stichting die een programmeertaal ontwikkelt waarmee je wiskundig kunt bewijzen dat software correct werkt.
• Waarom relevant: AI-agents nemen steeds vaker beslissingen met financiële of operationele gevolgen — wiskundig bewijs biedt een fundamenteel ander veiligheidsniveau dan testen alleen.
• Wat je ermee kunt: Als je AI-agents overweegt voor bedrijfsprocessen, vraag je leverancier hoe zij de correctheid van die agents garanderen.

Ik kwam dit bericht tegen via Amazon Science en het trok meteen mijn aandacht. Niet vanwege Amazon zelf, maar vanwege de onderliggende boodschap: testen is niet meer genoeg als je AI laat meebeslissen in je bedrijf. Amazon investeert daarom fors in een programmeertaal die wiskundig kan bewijzen dat software doet wat het moet doen.

Wat is er precies aan de hand?

Op 26 juli 2026 maakte Amazon bekend dat het investeert in de Lean Focused Research Organization — volgens Amazon de grootste donatie in de geschiedenis van die organisatie. Een concreet bedrag is niet genoemd.

Lean is een open-source programmeertaal die in 2013 is gestart door Leo de Moura. Het bijzondere: in Lean kun je niet alleen code schrijven, maar ook wiskundig bewijzen dat die code correct is. Niet "we hebben het getest en het lijkt te werken", maar "we hebben bewezen dat dit onder alle omstandigheden klopt". Dat klinkt misschien abstract, maar het verschil is fundamenteel.

Stel dat je een sluis bouwt. Testen is: we hebben water doorgelaten bij verschillende waterstanden en het ging goed. Bewijzen is: we hebben wiskundig aangetoond dat de sluis bij élke waterstand werkt, ook bij combinaties die we niet hebben geprobeerd. Dat verschil wordt belangrijk zodra de gevolgen van fouten groot zijn.

Waarom doet Amazon dit nu?

De timing is niet toevallig. AI-agents — software die zelfstandig beslissingen neemt en acties uitvoert — worden steeds vaker ingezet voor taken met echte consequenties. Denk aan het verplaatsen van geld, het goedkeuren van claims, of het aansturen van infrastructuur.

Amazon schrijft het zelf vrij helder op: "Testing checks the cases you thought of, but there is a fundamentally different approach: mathematical proof, which shows with certainty that a system cannot behave incorrectly." Vrij vertaald: testen controleert de scenario's waar jij aan dacht. Wiskundig bewijs laat zien dat het systeem zich nooit verkeerd kan gedragen.

Wat mij hier opvalt, is dat Amazon ervoor kiest om deze investering te doen via een onafhankelijke organisatie in plaats van intern. De reden die ze geven is transparantie: klanten, auditors en toezichthouders moeten de bewijstools zelf kunnen controleren. Dat vind ik een interessant signaal. Het suggereert dat Amazon verwacht dat toezichthouders hier op termijn naar gaan vragen.

Waar gebruikt Amazon het al?

Dit is geen toekomstmuziek. Amazon zet Lean al in voor meerdere producten:

Bedrock AgentCore

Hier wordt Lean-verificatie gebruikt om wiskundig te bewijzen dat AI-agents binnen vooraf vastgestelde grenzen blijven. Als je een agent bouwt die namens je bedrijf handelt, wil je weten dat die agent niet buiten zijn mandaat treedt.

SampCert

Een wiskundig bewezen implementatie van privacybescherming in AWS Clean Rooms. Dit is relevant voor bedrijven die data delen met partners maar privacygaranties nodig hebben.

Amazon Aurora

Een Amazon-wetenschapper gebruikte recent een combinatie van een taalmodel en Lean om de correctheid te bewijzen van wat Amazon omschrijft als hun "meest kritische protocol voor dataduurzaamheid". Dat lukte in een fractie van de tijd die het handmatig zou kosten.

Dat laatste voorbeeld vind ik eerlijk gezegd fascinerend. Een AI-model helpt bij het schrijven van wiskundige bewijzen, en die bewijzen worden vervolgens machinaal gecontroleerd. De AI doet het denkwerk, maar de wiskunde controleert of het klopt. Het is alsof je een stagiair een rapport laat schrijven en een accountant het laat aftekenen.

Wat betekent dit voor ondernemers?

Laat ik eerlijk zijn: als MKB-ondernemer ga je waarschijnlijk niet zelf met Lean aan de slag. Dat hoeft ook niet. Maar er zitten wel een paar ontwikkelingen in die je in de gaten wilt houden.

De betrouwbaarheidsvraag wordt concreter

Als je nu een AI-tool inzet voor klantenservice, boekhouding of voorraadbeheer, vertrouw je op de leverancier dat het goed werkt. Maar hoe weet je dat eigenlijk? De meeste antwoorden die je krijgt zijn variaties op "we hebben het uitgebreid getest". Wiskundig bewijs is een fundamenteel ander antwoord. Ik verwacht dat dit de komende jaren een onderscheidend punt wordt tussen leveranciers.

Toezicht gaat meebewegen

Amazon's keuze om via een onafhankelijke organisatie te werken — zodat toezichthouders de tools kunnen controleren — is veelzeggend. In de EU wordt met de AI Act al gewerkt aan eisen voor hoog-risico AI-systemen. Wiskundige verificatie past precies in dat plaatje. Kun je je voorstellen dat een toezichthouder straks vraagt: "Kunt u bewijzen dat uw AI-systeem binnen de regels blijft?" Dat is niet meer zo hypothetisch als het klinkt.

De combinatie AI + bewijs is nieuw

Wat mij bijzonder opvalt, is dat AI-modellen nu zelf worden ingezet om wiskundige bewijzen te produceren. Mistral bracht in maart 2026 Leanstral uit, een AI-agent specifiek ontworpen om code én wiskundige bewijzen te genereren in Lean. Die bewijzen zijn vervolgens machinaal controleerbaar. Dat maakt formele verificatie toegankelijker — niet alleen voor wiskundigen, maar potentieel voor reguliere softwareteams.

Het grotere plaatje

Lean heeft inmiddels een indrukwekkend ecosysteem. De wiskundebibliotheek Mathlib bevat 1,58 miljoen regels geverifieerde code, bijgedragen door meer dan 300 wiskundigen. Er zijn workshops, universitaire cursussen, en steeds meer bedrijven die ermee experimenteren. Microsoft Research gebruikt Lean bijvoorbeeld om cryptografische algoritmen te verifiëren.

Toch wil ik er een nuance bij plaatsen. Formele verificatie is niet nieuw — het bestaat al decennia in niches als luchtvaart en chipdesign. Wat wél nieuw is, is de ambitie om het breed toegankelijk te maken voor reguliere softwareontwikkeling. Of dat lukt, hangt af van hoe snel de tooling verbetert en hoeveel ontwikkelaars het daadwerkelijk gaan gebruiken. Dat is nog geen uitgemaakte zaak.

Voor mij is dit vooral een signaal dat de industrie begint in te zien dat "het werkt in onze tests" niet meer volstaat als AI-systemen echte beslissingen nemen. De vraag verschuift van "hebben we het getest?" naar "kunnen we het bewijzen?" En als ondernemer die AI inzet of overweegt in te zetten, is dat een verschuiving die je wilt volgen.