&Truth haalt 70 miljoen dollar aan startkapitaal op voor de bouw van een universele verificatiemachine voor code

&Truth, een vennootschap met een maatschappelijk doel die technologie ontwikkelt om wiskundig te bewijzen dat software veilig is, kwam op 29 oktober 2026 uit de stealthmodus. Het bedrijf maakte bekend dat het 70 miljoen dollar aan startkapitaal had opgehaald en plannen had om te bouwen wat het een universele verificatiemachine voor code noemt.

In de aankondiging van zijn lancering zei het bedrijf dat het begin 2026 was opgericht en 70 miljoen dollar aan startkapitaal had ontvangen van een groep die het omschreef als toonaangevende leiders op het gebied van AI-veiligheid en durfkapitaal. Het bedrijf zei dat het zijn verificatiemachine ontwikkelt om code in elke programmeertaal te lezen en wiskundig te bewijzen dat die veilig, beveiligd en correct is, met bewijzen die iedereen onafhankelijk kan controleren.

Bewijsautomatisering op basis van Lean

Formele verificatie bestaat al tientallen jaren, maar was voorheen ontoegankelijk en duur, aldus de aankondiging, omdat experts bewijzen handmatig moesten formuleren. Daardoor bleef de toepassing beperkt tot een handvol kritieke systemen. Volgens het bedrijf versnelt AI het werk aan formele bewijzen nu met een factor 100 of meer, en versnelt de technologie voor bewijsautomatisering het proces nog eens met een factor 100. Daardoor kan het genereren van bewijzen worden teruggebracht van jaren of maanden tot uren of minuten.

Het bedrijf beschreef ook de technologie die het een ‘specificatiefabriek’ noemt. Deze stelt bedrijven en ontwikkelaars volgens het bedrijf in staat om menselijke intenties en zakelijke vereisten op grote schaal om te zetten in nauwkeurige formele specificaties. Dat levert garanties op die onafhankelijk kunnen worden gecontroleerd, in plaats van te berusten op tests of claims van leveranciers.

&Truth bouwt voort op Lean, een opensourcesysteem voor bewijzen, en Mathlib, een bibliotheek met meer dan twee miljoen regels aan wiskundige definities en stellingen, en op opensourcetechnologieën zoals CSLib. Volgens het bedrijf is het doel een universele formele taal voor software: wiskundige modellen van programmeertalen en systemen, bewijstechnieken en nauwkeurige specificaties die geautomatiseerde verificatie in verschillende talen mogelijk maken. &Truth zei samen te werken met de Lean Focused Research Organization en van plan te zijn zijn fundamentele bibliotheken als open source beschikbaar te stellen.

Medeoprichter en mede-CEO Clark Barrett zei dat Lean en Mathlib AI een nauwkeurige taal boden om wiskundig te redeneren, maar dat software een vergelijkbare basis miste. Medeoprichter en Chief Science Officer Ilya Sergey zei dat vertrouwen in software moet berusten op onafhankelijk controleerbare bewijzen, en niet op het woord van een bedrijf.

Oprichters en twee hoofdkantoren

Barrett is de Corbel-hoogleraar informatica aan Stanford University, medeoprichter en codirecteur van het Stanford Center for AI Safety, directeur van het Stanford Center for Automated Reasoning, medeontwikkelaar van CSLib en projectleider van de geautomatiseerde redeneermotor cvc5. Sergey richtte het VERSE Lab op aan de National University of Singapore en was medeontwikkelaar van de opensourceverificateurs Veil en Velvet. Medeoprichter, mede-CEO en uitvoerend voorzitter Chris Hsu is lid van de strategische adviesraad van Lean FRO en voorzitter van Infinitude Foundation. Eerder was hij CEO van Kilometre Capital en managing director bij Citadel Investment Group.

In de aankondiging werden ook Gregory Malecha genoemd, die eerder leiding gaf aan het team voor formele methoden bij BlueRock Security en een van de belangrijkste architecten was van het verificatiekader BRiCk; Sebastian Ullrich, mede-architect van Lean 4 en medeoprichter van de Lean Focused Research Organization; Linus Lee, voormalig managing partner bij Kilometre Capital; en Drew Harman, voormalig commercieel directeur bij Fastino Labs en operating partner bij Insight Partners en Shasta Ventures. &Truth zei voort te bouwen op tientallen jaren onderzoek naar formele verificatie en geautomatiseerd redeneren aan Stanford University en de National University of Singapore.

Het Amerikaanse hoofdkantoor van &Truth staat in Palo Alto en het internationale hoofdkantoor in Singapore. Het bedrijf zei dat zijn kantoor daar aanzienlijk wordt uitgebreid voor onderzoek, engineering, productontwikkeling en commerciële activiteiten. Low Jin Yong, Senior Vice President en medehoofd van Digital Industry Singapore, zei in de aankondiging dat het hoofdkantoor de capaciteiten van Singapore op het gebied van vertrouwen en veiligheid zal versterken en het land zal positioneren als uitvalsbasis voor bedrijven die betrouwbare AI ontwikkelen.

Op de website van het bedrijf staat ook een rondetafelgesprek met Leonardo de Moura, de bedenker van Lean en VP en Distinguished Scientist bij AWS, en Simone Severini, lid van de strategische adviesraad van Lean FRO en Distinguished Engineer bij Google.

Begeleidende essays lichten de beweegredenen van het bedrijf toe

In een begeleidend essay van 29 oktober 2026 lichtte Hsu de ontwikkelingen toe die verificatie volgens het bedrijf urgent maken. Hij verwees daarbij naar uitspraken van Google-CEO Sundar Pichai, die zei dat inmiddels 75% van de nieuwe code bij Google door AI wordt gegenereerd en door engineers wordt goedgekeurd, en naar tests van Veracode uit 2026, waaruit bleek dat AI-modellen faalden bij bijna de helft van de programmeertaken waarbij beveiliging van belang was. Het essay verwijst ook naar een campagne in september 2026 waarbij een aanvaller honderden AI-agenten inzette om via kwetsbaarheden in veelgebruikte software voor printerbeheer 395 organisaties in 48 landen binnen te dringen, en naar een recordaantal van 14.959 softwarekwetsbaarheden dat in september 2026 werd gepubliceerd. Volgens het essay is dat 3,5 keer zoveel als het aantal dat een jaar eerder werd gepubliceerd.

Het essay beschrijft eerdere mijlpalen op het gebied van formele verificatie: het oorspronkelijke bewijs voor de seL4-microkernel vergde ongeveer 20 persoonsjaren aan werk van experts voor circa 8.700 regels code; in 2015 werd seL4 in het kader van DARPA’s HACMS-programma ingebouwd in Boeings Unmanned Little Bird-helikopter, waarvan een professioneel red team de vluchtbesturing niet kon kraken, zelfs niet na weken toegang te hebben gehad; en in september 2026 formaliseerde een door Anthropic ontwikkeld AI-model in 11 dagen in Lean het volledige bewijs van de laatste stelling van Fermat. Ook vermeldt het essay dat Kim Morrison, senior onderzoekssoftware-engineer bij de Lean FRO, eerder in 2026 met Claude van Anthropic en minimale menselijke begeleiding een Lean-versie van de compressiebibliotheek zlib bouwde en bewees dat die altijd exact de gegevens terugzet die ermee zijn gecomprimeerd.

Het essay citeert Lean-bedenker Leonardo de Moura: “Testen geeft vertrouwen. Een bewijs biedt zekerheid.”

In een tweede essay, gepubliceerd op 29 oktober 2026, legt Sergey uit hoe programmaverificatie werkt. Hij begint met Alan Turings artikel “Checking a Large Routine” uit 1949, waarin werd voorgesteld dat programmeurs hun code vergezellen van nauwkeurige beweringen die een controleprogramma afzonderlijk kan verifiëren. Het essay beschrijft specificaties, lusinvarianten en bewijzen die in Lean worden gecontroleerd, en stelt dat &Truth ontwikkelaars onafhankelijk controleerbaar bewijs wil laten verkrijgen, zoals een formeel bewijs in Lean, tegen kosten die verificatie tot een vast onderdeel van de ontwikkeling maken.

&Truth beschrijft zijn langetermijnvisie als een verschuiving van “vibe-coding” naar “veri-coding”, waarbij door AI gegenereerde code vóór implementatie wiskundig wordt geverifieerd, AI-agenten werken in omgevingen waarvan de begrenzing formeel kan worden bewezen, verouderde software veilig wordt gemoderniseerd en kritieke infrastructuur wordt beschermd met onafhankelijk controleerbare wiskundige garanties.