Terwijl kunstmatige intelligentie de ontwikkeling van software hervormt, gokt een kleine startup erop dat het volgende grote knelpunt in de sector niet het schrijven van code zal zijn, maar dat het erop gaat vertrouwen.
Stellingeen in San Francisco gevestigd bedrijf dat voortkwam uit Y Combinator’s Lente 2025 batch heeft dinsdag aangekondigd dat het $6 miljoen aan startfinanciering heeft opgehaald om geautomatiseerde tools te bouwen die de juistheid van door AI gegenereerde software verifiëren. Khosla Ventures leidde de ronde, met deelname van Y-combinator, e14, SAIF, Halcyonen engelinvesteerders, waaronder Blake Borgesson, mede-oprichter van Recursion Pharmaceuticals, en Arthur Breitman, mede-oprichter van blockchain-platform Tezos.
De investering komt op een cruciaal moment. AI-coderingsassistenten van bedrijven zoals GitHub, AmazoneEn Googlen genereren nu jaarlijks miljarden regels code. De acceptatie door bedrijven versnelt. Maar het vermogen om te verifiëren dat door AI geschreven software daadwerkelijk werkt zoals bedoeld, heeft geen gelijke tred gehouden – waardoor er is ontstaan wat de oprichters van Theorem omschrijven als een steeds groter wordende ‘toezichtskloof’ die een bedreiging vormt voor de kritieke infrastructuur, van financiële systemen tot elektriciteitsnetwerken.
“We zijn er al”, zei Jason Gross, medeoprichter van Theorem, toen we vroegen of de door AI gegenereerde code de menselijke beoordelingscapaciteit overtreft. “Als je mij zou vragen om 60.000 regels code te beoordelen, zou ik niet weten hoe ik dat moet doen.”
Waarom AI code sneller schrijft dan mensen deze kunnen verifiëren
De kerntechnologie van Theorem combineert formele verificatie – een wiskundige techniek die bewijst dat software zich precies gedraagt zoals gespecificeerd – met AI-modellen die zijn getraind om automatisch proefdrukken te genereren en te controleren. De aanpak transformeert een proces dat historisch gezien jaren van engineering op PhD-niveau vereiste, in iets dat volgens het bedrijf in weken of zelfs dagen kan worden voltooid.
Formele verificatie bestaat al tientallen jaren, maar bleef beperkt tot de meest bedrijfskritische toepassingen: luchtvaartelektronicasystemen, kernreactorcontroles en cryptografische protocollen. De onbetaalbare kosten van de techniek (waarvoor vaak acht regels wiskundig bewijs nodig zijn voor elke regel code) maakten deze onpraktisch voor reguliere softwareontwikkeling.
Gross weet dit uit de eerste hand. Voordat hij Theorem oprichtte, promoveerde hij aan het MIT op het gebied van verificatie cryptografiecode die nu het HTTPS-beveiligingsprotocol aanstuurt dagelijks biljoenen internetverbindingen beschermen. Dat project kostte naar zijn schatting vijftien mensjaren aan arbeid.
“Niemand geeft er de voorkeur aan om onjuiste code te hebben,” zei Gross. “Softwareverificatie was voorheen gewoon niet rendabel. Bewijzen werden vroeger geschreven door ingenieurs op PhD-niveau. Nu schrijft AI alles.”
Hoe formele verificatie de bugs opspoort die bij traditioneel testen over het hoofd worden gezien
Het systeem van Stelling werkt volgens een principe dat Gross ‘fractioneel bewijsdecompositie’ noemt. In plaats van elk mogelijk gedrag uitvoerig te testen – rekenkundig onhaalbaar voor complexe software – wijst de technologie verificatiemiddelen toe in verhouding tot het belang van elke codecomponent.
De aanpak heeft onlangs een bug geïdentificeerd die voorbij de tests bij Anthropic is geglipt, het AI-veiligheidsbedrijf achter de Claude-chatbot. Gross zei dat de techniek ontwikkelaars helpt “hun bugs nu op te sporen zonder veel rekenkracht te verbruiken.”
In een recente technische demonstratie genaamd SFBench gebruikte Theorem AI om 1.276 problemen van Rocq (een formele proefassistent) naar Lean (een andere verificatietaal) te vertalen, en bewees vervolgens automatisch dat elke vertaling gelijkwaardig was aan het origineel. Het bedrijf schat dat een menselijk team ongeveer 2,7 mensjaren nodig zou hebben gehad om hetzelfde werk te voltooien.
“Iedereen kan agenten parallel laten draaien, maar we kunnen ze ook sequentieel uitvoeren”, legt Gross uit, waarbij hij opmerkt dat de architectuur van Theorem omgaat met onderling afhankelijke code – waarbij oplossingen op elkaar voortbouwen over tientallen bestanden – waardoor conventionele AI-codeeragenten worden uitgeschakeld die beperkt zijn door contextvensters.
Hoe een bedrijf een specificatie van 1500 pagina’s omzet in 16.000 regels vertrouwde code
De startup werkt al met klanten in AI-onderzoekslaboratoria, elektronische ontwerpautomatisering en GPU-versneld computergebruik. Eén casestudy illustreert de praktische waarde van de technologie.
Een klant kwam naar Theorem met een PDF-specificatie van 1500 pagina’s en een oudere software-implementatie die geplaagd werd door geheugenlekken, crashes en andere ongrijpbare bugs. Hun meest urgente probleem: het verbeteren van de prestaties van 10 megabit per seconde naar 1 gigabit per seconde – een honderdvoudige toename – zonder extra fouten te introduceren.
Het systeem van Theorem genereerde 16.000 regels productiecode, die de klant implementeerde zonder deze ooit handmatig te herzien. Het vertrouwen kwam van een compacte uitvoerbare specificatie – een paar honderd regels die het enorme PDF-document generaliseerden – gecombineerd met een gelijkwaardigheidscontrolesysteem dat verifieerde dat de nieuwe implementatie overeenkwam met het beoogde gedrag.
“Nu hebben ze een parser van productiekwaliteit die werkt op 1 Gbps en die ze kunnen inzetten met het vertrouwen dat er tijdens het parseren geen informatie verloren gaat”, aldus Gross.
De beveiligingsrisico’s die op de loer liggen in door AI gegenereerde software voor kritieke infrastructuur
De financieringsaankondiging komt op een moment dat beleidsmakers en technologen de betrouwbaarheid van AI-systemen die zijn ingebed in kritieke infrastructuur steeds meer onder de loep nemen. Software controleert nu al de financiële markten, medische apparatuur, transportnetwerken en elektriciteitsnetwerken. AI versnelt hoe snel software evolueert – en hoe gemakkelijk subtiele bugs zich kunnen verspreiden.
Gross omschrijft de uitdaging in termen van veiligheid. Omdat AI het goedkoper maakt om kwetsbaarheden te vinden en te exploiteren, hebben verdedigers behoefte aan wat hij ‘asymmetrische verdediging’ noemt: bescherming die schaalbaar is zonder proportionele toename van de middelen.
“Softwarebeveiliging is een delicaat evenwicht tussen aanval en verdediging”, zei hij. “Met AI-hacking dalen de kosten van het hacken van een systeem scherp. De enige haalbare oplossing is asymmetrische verdediging. Als we een softwarebeveiligingsoplossing willen die meer dan een paar generaties aan modelverbeteringen meegaat, zal dat via verificatie gebeuren.”
Op de vraag of toezichthouders formele verificatie van door AI gegenereerde code in kritieke systemen moeten verplichten, antwoordde Gross scherp: “Nu formele verificatie goedkoop genoeg is, kan het als grove nalatigheid worden beschouwd om deze niet te gebruiken voor garanties over kritieke systemen.”
Wat Theorem onderscheidt van andere startups voor AI-codeverificatie
Theorem betreedt een markt waar talloze startups en onderzoekslaboratoria het snijvlak van AI en formele verificatie onderzoeken. De differentiatie van het bedrijf, zo betoogt Gross, ligt in de unieke focus op het opschalen van softwaretoezicht in plaats van verificatie toe te passen op wiskunde of andere domeinen.
“Onze tools zijn nuttig voor systeemengineeringteams die dicht bij het metaal werken en die garanties op juistheid nodig hebben voordat ze wijzigingen kunnen samenvoegen”, zei hij.
Het oprichtende team weerspiegelt die technische oriëntatie. Gross brengt diepgaande expertise in op het gebied van programmeertaaltheorie en een staat van dienst op het gebied van het op grote schaal inzetten van geverifieerde code in productie. Medeoprichter Rajashree Agrawal, een onderzoeksingenieur op het gebied van machine learning, richt zich op het trainen van de AI-modellen die de verificatiepijplijn aandrijven.
“We werken aan een formele programma-redenering, zodat iedereen niet alleen toezicht kan houden op het werk van een gemiddelde AI op software-ingenieursniveau, maar ook echt de mogelijkheden van een AI op Linus Torvalds-niveau kan benutten”, zei Agrawal, verwijzend naar de legendarische maker van Linux.
De race om de AI-code te verifiëren voordat deze alles controleert
Stelling is van plan de financiering te gebruiken om zijn team uit te breiden, de computerbronnen voor het trainen van verificatiemodellen te vergroten en nieuwe industrieën te betreden, waaronder robotica, hernieuwbare energie, cryptocurrency en medicijnsynthese. Het bedrijf heeft momenteel vier mensen in dienst.
De opkomst van de startup duidt op een verschuiving in de manier waarop leiders op het gebied van bedrijfstechnologie AI-coderingstools mogelijk moeten evalueren. De eerste golf van AI-ondersteunde ontwikkeling beloofde productiviteitswinst: meer code, sneller. Stelling houdt in dat de volgende golf iets anders zal vereisen: wiskundig bewijs dat snelheid niet ten koste gaat van de veiligheid.
Gross schetst de inzet in grimmige bewoordingen. AI-systemen verbeteren exponentieel. Als dat traject standhoudt, gelooft hij dat bovenmenselijke software-engineering onvermijdelijk is – in staat om systemen te ontwerpen die complexer zijn dan alles wat mensen ooit hebben gebouwd.
‘En zonder een radicaal andere economische manier van toezicht,’ zei hij, ‘zullen we uiteindelijk systemen inzetten waar we geen controle over hebben.’
De machines schrijven de code. Nu moet iemand zijn werk controleren.
