Terwijl kunstmatige intelligentie de ontwikkeling van software hervormt, gokt een kleine startup erop dat de volgende grote hindernis in de industrie niet het schrijven van code zal zijn; ze zullen het geloven.
Stellingeen in San Francisco gevestigd bedrijf dat voortkwam uit Y Combinator’s Lente 2025 batch heeft dinsdag aangekondigd dat het 6 miljoen dollar aan startfinanciering heeft opgehaald om geautomatiseerde tools te bouwen die de juistheid van door AI gegenereerde software verifiëren. Khosla-ondernemingen leidt de ronde, met deelname van Y-combinator, e14, SAIF, Kalmen engelinvesteerders, waaronder Blake Borgesson, mede-oprichter van Recursion Pharmaceuticals, en Arthur Breitman, mede-oprichter van blockchain-platform Tezos.
De investering komt op een heel belangrijk moment. AI-coderingsassistent van een soortgelijk bedrijf GitHub, AmazoneEn Googlen het produceert nu jaarlijks miljarden regels code. De acceptatie door bedrijven versnelt. Maar het vermogen om te verifiëren dat software die met AI is gemaakt daadwerkelijk werkt zoals bedoeld, is nog niet aangeslagen – waardoor er is ontstaan wat de oprichters van Theorem omschrijven als een groeiende ‘toezichtskloof’ die een bedreiging vormt voor de kritieke infrastructuur, van financiële systemen tot het elektriciteitsnet.
“We zijn er al”, zei Jason Gross, medeoprichter van Theorem, toen we vroegen of de door AI gegenereerde code de menselijke beoordelingscapaciteit te boven gaat. “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 kunnen verifiëren
De kerntechnologie van Theorem combineert formele verificatie – wiskundige technieken die bewijzen dat software zich precies gedraagt zoals gespecificeerd – met AI-modellen die zijn getraind om automatisch bewijzen te genereren en te controleren. Deze aanpak transformeert een proces dat historisch gezien jaren van engineering op PhD-niveau vereiste, in iets dat volgens het bedrijf binnen enkele weken of zelfs dagen kan worden voltooid.
Formele verificatie bestaat al tientallen jaren, maar is nog steeds beperkt tot de meest kritische toepassingen: luchtvaartelektronicasystemen, controle van kernreactoren en cryptografische protocollen. De hoge kosten van deze techniek (waarvoor vaak acht regels wiskundig bewijs nodig zijn voor elke regel code) maken deze onpraktisch voor algemene softwareontwikkeling.
Gross weet dit uit de eerste hand. Voordat hij Theorem oprichtte, promoveerde hij aan het MIT op verificatie cryptografische code die nu het HTTPS-beveiligingsprotocol ondersteunt beschermt elke dag biljoenen internetverbindingen. Hij schatte dat het project vijftien manjaren arbeid vergde.
“Niemand kiest de verkeerde code”, zei Gross. “Vroeger was softwareverificatie oneconomisch. Vroeger werd het bewijs geschreven door ingenieurs op PhD-niveau. Nu schrijft AI het allemaal.”
Hoe formele verificatie bugs opspoort die bij traditioneel testen over het hoofd worden gezien
Het stellingensysteem werkt volgens een principe dat Gross “fractioneel bewijsdecompositie” noemt. In plaats van elk mogelijk gedrag uitvoerig te testen – wat rekenkundig onhaalbaar is voor complexe software – wijst deze technologie verificatiebronnen toe in verhouding tot het belang van elke codecomponent.
De aanpak heeft onlangs een bug geïdentificeerd die aan de tests bij Anthropic, het AI-beveiligingsbedrijf achter de chatbot Claude, ontsnapte. Gross zegt dat deze techniek ontwikkelaars helpt “hun bugs nu op te sporen zonder veel rekenkracht uit te geven.”
In een recente technische demonstratie genaamd SFBench gebruikte Teorem 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 heeft om hetzelfde werk te voltooien.
“Iedereen kan agenten parallel laten draaien, maar we kunnen ze ook sequentieel laten draaien”, legt Gross uit, waarbij hij opmerkt dat de architectuur van Theorem omgaat met onderling afhankelijke code – waarbij oplossingen op elkaar voortbouwen in tientallen bestanden – waardoor conventionele AI-codeeragenten beperkt worden door contextvensters.
Hoe een bedrijf een specificatie van 1500 pagina’s omzet in 16.000 regels vertrouwde code
De startup heeft met klanten samengewerkt in AI-onderzoekslaboratoria, elektronische ontwerpautomatisering en GPU-versneld computergebruik. Een case study illustreert de praktische waarde van deze 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 moeilijk te begrijpen bugs. Hun meest dringende probleem: de prestaties verhogen van 10 megabit per seconde naar 1 gigabit per seconde – een honderdvoudige verbetering – zonder extra fouten te introduceren.
Het Theorem-systeem genereerde 16.000 regels productiecode, die de klant implementeerde zonder deze ooit handmatig te herzien. Dit vertrouwen komt voort uit een beknopte uitvoerbare specificatie – een paar honderd regels die grote PDF-documenten generaliseren – gecombineerd met een reeks gelijkheidscontroles die verifiëren dat de nieuwe implementatie voldoet aan het gewenste gedrag.
“Nu hebben ze een parser van productiekwaliteit die werkt op 1 Gbps en die ze kunnen inzetten met het vertrouwen dat er geen informatie verloren gaat tijdens het parseren”, aldus Gross.
Beveiligingsrisico’s liggen op de loer in door AI gegenereerde software voor kritieke infrastructuur
De aankondiging van de financiering komt omdat beleidsmakers en technologie-experts 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 elektriciteitsnetten. AI versnelt de softwareontwikkeling – en hoe gemakkelijk subtiele bugs zich verspreiden.
Gross omschrijft de uitdaging in termen van veiligheid. Omdat AI het gemakkelijker maakt om kwetsbaarheden te vinden en te exploiteren, hebben verdedigers behoefte aan wat zij ‘asymmetrische verdedigingen’ noemen: beschermingen die kunnen worden uitgebreid zonder een 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 modelverbeteringen kan overleven, is de oplossing via verificatie.”
Op de vraag of toezichthouders formele verificatie van door AI gegenereerde code in kritieke systemen moeten eisen, gaf Gross een resoluut antwoord: “Nu formele verificatie goedkoop genoeg is, kan het als grove nalatigheid worden beschouwd om deze niet als onderpand voor kritieke systemen te gebruiken.”
Wat Theorem onderscheidt van andere startups voor AI-codeverificatie
Theorem betreedt een markt waar veel startups en onderzoekslaboratoria het kruispunt tussen AI en formele verificatie onderzoeken. Het onderscheid van het bedrijf ligt volgens Gross in de unieke focus op het verbeteren van softwaremonitoring versus het toepassen van verificatie op wiskunde of andere domeinen.
“Onze tool is nuttig voor systeemengineeringteams die dicht bij het metaal werken en zekerheid willen hebben over de juistheid voordat ze wijzigingen kunnen samenvoegen”, zegt hij.
Het oprichtende team weerspiegelt die technische oriëntatie. Gross brengt diepgaande expertise in op het gebied van programmeertaaltheorie en een track record 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 AI-modellen die verificatietrajecten ondersteunen.
“We werken aan een formele programma-redenering, zodat iedereen niet alleen het typische AI-werk op software-ingenieursniveau kan overzien, maar ook echt de AI-mogelijkheden van Linus Torvalds kan benutten,” zei Agrawal, verwijzend naar de legendarische maker van Linux.
De race is begonnen om de AI-code te verifiëren voordat alles wordt gecontroleerd
Stelling is van plan de financiering te gebruiken om zijn team uit te breiden, de computermiddelen voor het trainen van verificatiemodellen te vergroten en nieuwe industrieën aan te moedigen, waaronder robotica, hernieuwbare energie, cryptocurrency en medicijnsynthese. Het bedrijf heeft momenteel vier mensen in dienst.
De opkomst van deze startups duidt op een verandering in de manier waarop leiders op het gebied van bedrijfstechnologie AI-coderingstools moeten evalueren. De eerste golf van AI-ondersteunde ontwikkeling beloofde een hogere productiviteit: meer code, sneller. De stelling is dat de volgende golf iets anders zal vereisen: wiskundig bewijs dat snelheid niet ten koste gaat van de veiligheid.
Gross schetst zijn inzet grimmig. AI-systemen verbeteren exponentieel. Als dit zo doorgaat, gelooft hij dat bovenmenselijke software-engineering onvermijdelijk zal zijn – in staat om systemen te ontwerpen die complexer zijn dan alles wat mensen ooit hebben gemaakt.
“En zonder radicaal ander economisch toezicht,” zei hij, “zullen we uiteindelijk een systeem implementeren waar we geen controle over hebben.”
De machine schrijft code. Nu moet iemand het werk controleren.
