&Truth tar in 70 miljoner dollar i såddkapital för att bygga en universell verifieringsmaskin för kod

&Truth, ett allmännyttigt bolag som utvecklar teknik för att matematiskt bevisa att programvara är säker, lämnade den 29 oktober 2026 sin utvecklingsfas i hemlighet och offentliggjorde att bolaget tagit in 70 miljoner dollar i såddkapital samt att det planerar att bygga vad det kallar en universell verifieringsmaskin för kod.

I annonseringen av lanseringen uppgav bolaget att det grundades i början av 2026 och finansierades med 70 miljoner dollar i såddkapital från en grupp som det beskrev som ledande aktörer inom AI-säkerhet och riskkapital, vilka bidragit till att forma området. Bolaget uppgav att verifieringsmaskinen utvecklas för att kunna läsa kod i alla programmeringsspråk och matematiskt bevisa att den är säker, skyddad och korrekt, med bevis som vem som helst kan kontrollera oberoende.

Automatisering av bevis med Lean som grund

Formell verifiering har funnits i årtionden, men har tidigare varit otillgänglig och kostsam, enligt annonseringen, eftersom experter var tvungna att formulera bevis manuellt. Därför har metoden varit begränsad till ett fåtal kritiska system. Bolaget uppgav att AI nu påskyndar arbetet med formella bevis med 100 gånger eller mer och att dess teknik för automatisering av bevisprocessen ger ytterligare 100 gångers hastighetsökning, vilket minskar tiden för att ta fram bevis från år eller månader till timmar eller minuter.

Bolaget beskrev också vad det kallar teknik för en ”specifikationsfabrik”, som enligt bolaget gör det möjligt för företag och utvecklare att i stor skala omvandla mänskliga avsikter och affärskrav till precisa formella specifikationer. Resultatet är garantier som kan kontrolleras oberoende, i stället för att bygga på tester eller leverantörers påståenden.

&Truth bygger vidare på Lean, ett system för bevis med öppen källkod, och Mathlib, ett bibliotek med över två miljoner rader matematiska definitioner och satser, tillsammans med teknik med öppen källkod, däribland CSLib. Enligt bolaget är målet att skapa ett universellt formellt språk för programvara: matematiska modeller av programmeringsspråk och system, bevistekniker och precisa specifikationer som möjliggör automatiserad verifiering mellan olika språk. &Truth uppgav att bolaget samarbetar med Lean Focused Research Organization och avser att publicera sina grundläggande bibliotek som öppen källkod.

Medgrundaren och vd:n Clark Barrett sade att Lean och Mathlib gav AI ett precist språk för matematiska resonemang, medan programvara saknat en motsvarande grund. Medgrundaren och forskningschefen Ilya Sergey sade att tilliten till programvara bör vila på bevis som kan kontrolleras oberoende, inte på vad ett företag säger.

Grundare och två huvudkontor

Barrett är Corbel-professor i datavetenskap vid Stanford University, grundande meddirektör för Stanford Center for AI Safety, chef för Stanford Center for Automated Reasoning, medskapare av CSLib och projektledare för den automatiserade resonemangsmotorn cvc5. Sergey grundade VERSE Lab vid National University of Singapore och var med och skapade verifieringsverktygen Veil och Velvet, som har öppen källkod. Medgrundaren, vd:n och styrelseordföranden Chris Hsu ingår i Lean FRO Strategic Advisory Board och är ordförande för Infinitude Foundation. Tidigare var han vd för Kilometre Capital och managing director på Citadel Investment Group.

I annonseringen nämndes också Gregory Malecha, som tidigare ledde arbetet med formella metoder på BlueRock Security och var en av huvudarkitekterna bakom verifieringsramverket BRiCk; Sebastian Ullrich, en av arkitekterna bakom Lean 4 och medgrundare av Lean Focused Research Organization; Linus Lee, tidigare managing partner på Kilometre Capital; samt Drew Harman, tidigare kommersiell chef på Fastino Labs och operativ partner på Insight Partners och Shasta Ventures. &Truth uppgav att bolaget bygger vidare på årtionden av forskning om formell verifiering och automatiserat resonemang vid Stanford University och National University of Singapore.

&Truths huvudkontor i USA ligger i Palo Alto och det internationella huvudkontoret ligger i Singapore. Där kommer bolagets kontor enligt uppgift att utökas betydligt inom forskning, teknik, produktutveckling och marknadsintroduktion. Low Jin Yong, Senior Vice President och medchef för Digital Industry Singapore, sade i annonseringen att huvudkontoret kommer att fördjupa Singapores förmåga att skapa tillit och säkerhet och stärka landets ställning som bas för företag som utvecklar tillförlitlig AI.

På bolagets webbplats finns också ett rundabordssamtal med Leonardo de Moura, Lean-skaparen och vice vd samt framstående forskare på AWS, och Simone Severini, ledamot av Lean FRO Strategic Advisory Board och framstående ingenjör på Google.

Kompletterande essäer förklarar bolagets motiv

I en kompletterande essä daterad den 29 oktober 2026 beskrev Hsu de trender som enligt bolaget gör verifiering brådskande. Han hänvisade till uttalanden från Googles vd Sundar Pichai om att 75 % av den nya koden på Google nu genereras av AI och godkänns av ingenjörer, samt till Veracodes tester från 2026, som visade att AI-modeller misslyckades med nästan hälften av de kodningsuppgifter där säkerhet var viktig. Essän tar också upp en kampanj i september 2026 då en angripare använde hundratals AI-agenter för att angripa 395 organisationer i 48 länder genom sårbarheter i allmänt använda program för utskriftshantering, och att rekordmånga 14 959 sårbarheter i programvara publicerades i september 2026 – 3,5 gånger så många som året innan.

I essän återges tidigare milstolpar inom formell verifiering: det ursprungliga beviset för mikrokärnan seL4 krävde ungefär 20 personår av expertarbete för cirka 8 700 kodrader; 2015 byggdes seL4, inom ramen för DARPA:s HACMS-program, in i Boeings obemannade helikopter Unmanned Little Bird, vars flygkontroller ett professionellt red team inte kunde forcera trots flera veckors tillgång; och i september 2026 formaliserade en AI-modell utvecklad av Anthropic hela beviset för Fermats stora sats i Lean på 11 dagar. Det nämns också att Kim Morrison, senior forskningsprogramvaruingenjör vid Lean FRO, tidigare under 2026 använde Anthropics Claude med minimal mänsklig vägledning för att skapa en Lean-version av komprimeringsbiblioteket zlib och bevisa att det alltid återställer exakt de data som det komprimerade.

I essän citeras Lean-skaparen Leonardo de Moura: ”Testning skapar förtroende. Bevis ger en garanti.”

I en andra essä, publicerad den 29 oktober 2026, förklarar Sergey hur programverifiering fungerar. Han börjar med Alan Turings artikel ”Checking a Large Routine” från 1949, där Turing föreslog att programmerare skulle åtfölja sin kod med precisa påståenden som en kontrollör kunde verifiera var för sig. Essän beskriver specifikationer, loopinvarianter och bevis som kontrolleras i Lean, och anger att &Truth strävar efter att utvecklare ska kunna få oberoende verifierbara belägg, till exempel ett formellt bevis i Lean, till en kostnad som gör verifiering till en rutinmässig del av utvecklingsarbetet.

&Truth beskriver sin långsiktiga vision som en övergång från ”vibe-kodning” till ”veri-kodning”, där AI-genererad kod verifieras matematiskt före driftsättning, AI-agenter verkar i miljöer där deras handlingsutrymme bevisligen är begränsat, äldre programvara moderniseras på ett säkert sätt och kritisk infrastruktur skyddas av matematiska garantier som kan kontrolleras oberoende.