&Truth rejser 70 mio. dollar i seed-finansiering til at bygge en universel verifikationsmaskine til kode

&Truth, et selskab med almennyttigt formål, der udvikler teknologi til matematisk at bevise, at software er sikker, trådte frem fra stealthfasen den 29. oktober 2026. Selskabet offentliggjorde en seed-finansiering på 70 mio. dollar og en plan om at bygge det, som det kalder en universel verifikationsmaskine til kode.

I sin lanceringserklæring oplyste virksomheden, at den blev grundlagt i begyndelsen af 2026 og modtog 70 mio. dollar i seedkapital fra en gruppe, som den beskrev som toneangivende ledere inden for AI-sikkerhed og venturekapital. Virksomheden sagde, at den er ved at udvikle sin verifikationsmaskine, så den kan læse kode i alle programmeringssprog og matematisk bevise, at den er sikker, tryg og korrekt, med beviser, som enhver selvstændigt kan kontrollere.

Automatisering af beviser baseret på Lean

Formel verifikation har eksisteret i årtier, men var tidligere utilgængelig og dyr, lød det i meddelelsen, fordi eksperter måtte udarbejde beviserne manuelt, hvilket begrænsede anvendelsen til en håndfuld kritiske systemer. Virksomheden sagde, at AI nu fremskynder arbejdet med formelle beviser med 100 gange eller mere, og at dens teknologi til automatisering af beviser fremskynder processen yderligere 100 gange, så udarbejdelsen af beviser går fra år eller måneder til timer eller minutter.

Virksomheden beskrev også det, den kalder en “specifikationsfabrik”, som ifølge den gør det muligt for virksomheder og udviklere i stor skala at omsætte menneskelige intentioner og forretningskrav til præcise formelle specifikationer. Det giver garantier, der kan kontrolleres uafhængigt, i stedet for at man må forlade sig på test eller leverandørpåstande.

&Truth bygger videre på Lean, et open source-bevissystem, og Mathlib, et bibliotek med mere end to millioner linjer matematiske definitioner og sætninger, samt open source-teknologier, herunder CSLib. Ifølge virksomheden er målet at skabe et universelt formelt vokabular for software: matematiske modeller af programmeringssprog og systemer, bevisteknikker og præcise specifikationer, der muliggør automatiseret verifikation på tværs af sprog. &Truth oplyste, at virksomheden samarbejder med Lean Focused Research Organization og har til hensigt at udgive sine grundlæggende biblioteker som open source.

Medstifter og fælles administrerende direktør Clark Barrett sagde, at Lean og Mathlib gav AI et præcist sprog til at ræsonnere matematisk, og at software hidtil har manglet et tilsvarende fundament. Medstifter og videnskabelig chef Ilya Sergey sagde, at tilliden til software bør bygge på beviser, der kan kontrolleres uafhængigt, snarere end på et hvilket som helst selskabs ord.

Grundlæggere og to hovedkontorer

Barrett er Corbel-professor i datalogi ved Stanford University, stiftende meddirektør for Stanford Center for AI Safety, direktør for Stanford Center for Automated Reasoning, medskaber af CSLib og projektleder for den automatiserede ræsonneringsmotor cvc5. Sergey grundlagde VERSE Lab ved National University of Singapore og var med til at skabe open source-verifikationsværktøjerne Veil og Velvet. Medstifter, fælles administrerende direktør og bestyrelsesformand Chris Hsu er medlem af Lean FRO Strategic Advisory Board og præsident for Infinitude Foundation. Tidligere var han administrerende direktør for Kilometre Capital og managing director hos Citadel Investment Group.

Meddelelsen nævnte også Gregory Malecha, der tidligere ledede arbejdet med formelle metoder hos BlueRock Security og var en central arkitekt bag verifikationsrammeværket BRiCk; Sebastian Ullrich, medarkitekt bag Lean 4 og medstifter af Lean Focused Research Organization; Linus Lee, tidligere managing partner hos Kilometre Capital; og Drew Harman, tidligere kommerciel direktør hos Fastino Labs og operating partner hos Insight Partners og Shasta Ventures. &Truth sagde, at virksomheden bygger videre på årtiers forskning i formel verifikation og automatiseret ræsonnering ved Stanford University og National University of Singapore.

&Truths hovedkontor i USA ligger i Palo Alto, og det internationale hovedkontor ligger i Singapore. Her vil virksomhedens kontor ifølge den blive udvidet betydeligt inden for forskning, ingeniørarbejde, produktudvikling og kommerciel lancering. Low Jin Yong, senior vicepræsident og medchef for Digital Industry Singapore, sagde i meddelelsen, at hovedkontoret vil styrke Singapores kapacitet inden for tillid og sikkerhed og gøre landet til en stærkere base for virksomheder, der udvikler pålidelig AI.

Virksomhedens hjemmeside indeholder også en rundbordsdiskussion med Leonardo de Moura, opfinderen af Lean og vicepræsident samt Distinguished Scientist hos AWS, og Simone Severini, medlem af Lean FRO Strategic Advisory Board og Distinguished Engineer hos Google.

Ledsagende essays uddyber virksomhedens begrundelse

I et ledsagende essay dateret 29. oktober 2026 beskrev Hsu de tendenser, som virksomheden mener gør verifikation presserende. Han henviste til udtalelser fra Googles administrerende direktør Sundar Pichai om, at 75 % af den nye kode hos Google nu genereres af AI og godkendes af ingeniører, samt Veracodes test fra 2026, som viste, at AI-modeller fejlede i næsten halvdelen af de kodningsopgaver, hvor sikkerhed var vigtig. Essayet henviser også til en kampagne i september 2026, hvor en angriber indsatte hundredvis af AI-agenter til at trænge ind i 395 organisationer i 48 lande ved at udnytte sårbarheder i udbredt software til printstyring, samt til det rekordhøje antal på 14.959 softwaresårbarheder offentliggjort i september 2026, hvilket ifølge essayet var 3,5 gange så mange som året før.

Essayet fortæller om tidligere milepæle inden for formel verifikation: Det oprindelige bevis for seL4-mikrokernen krævede omkring 20 personårs ekspertarbejde for cirka 8.700 kodelinjer; i 2015 blev seL4 som led i DARPA’s HACMS-program indbygget i Boeings ubemandede Little Bird-helikopter, hvis flyvestyring et professionelt rødt hold med flere ugers adgang ikke kunne bryde ind i; og i september 2026 formaliserede en AI-model udviklet af Anthropic det fuldstændige bevis for Fermats sidste sætning i Lean på 11 dage. Essayet bemærker også, at Kim Morrison, senior softwareingeniør inden for forskning ved Lean FRO, tidligere i 2026 brugte Anthropics Claude med minimal menneskelig vejledning til at bygge en Lean-version af zlib-komprimeringsbiblioteket og bevise, at det altid gendanner præcis de data, det komprimerede.

Essayet citerer Lean-skaberen Leonardo de Moura: “Test giver tillid. Beviser giver en garanti.”

I et andet essay, der blev offentliggjort den 29. oktober 2026, forklarer Sergey, hvordan programverifikation fungerer, med udgangspunkt i Alan Turings artikel fra 1949, “Checking a Large Routine”, som foreslog, at programmører skulle ledsage deres kode med præcise påstande, som en kontrollør kunne verificere hver for sig. Essayet beskriver specifikationer, løkkeinvarianter og beviser, der kontrolleres i Lean, og fastslår, at &Truths mål er, at udviklere kan få uafhængigt kontrollerbar dokumentation, for eksempel et formelt bevis i Lean, til en pris, der gør verifikation til en rutinemæssig del af udviklingsarbejdet.

&Truth beskriver sin langsigtede vision som et skifte fra “vibe-kodning” til “veri-kodning”, hvor AI-genereret kode verificeres matematisk før udrulning, AI-agenter opererer i miljøer med dokumenterbare begrænsninger, ældre software moderniseres sikkert, og kritisk infrastruktur beskyttes af matematisk sikkerhed, der kan kontrolleres uafhængigt.