&Truth henter 70 millioner dollar i såkornfinansiering for å bygge en universell verifikasjonsmaskin for kode

&Truth, et allmennyttig selskap som utvikler teknologi for matematisk å bevise at programvare er trygg, trådte fram fra stealth-modus 29. oktober 2026. Selskapet opplyste at det hadde hentet 70 millioner dollar i såkornfinansiering, og la fram en plan om å bygge det selskapet kaller en universell verifikasjonsmaskin for kode.

I kunngjøringen av lanseringen opplyste selskapet at det ble grunnlagt tidlig i 2026 og fikk 70 millioner dollar i såkornkapital fra en gruppe det beskrev som toneangivende aktører innen AI-sikkerhet og risikokapital. Selskapet sa at verifikasjonsmaskinen utvikles for å kunne lese kode i alle programmeringsspråk og matematisk bevise at den er trygg, sikker og korrekt, med bevis som hvem som helst kan kontrollere uavhengig.

Automatisering av bevisføring basert på Lean

Formell verifikasjon har eksistert i flere tiår, men har tidligere vært utilgjengelig og kostbar, ifølge kunngjøringen, fordi eksperter måtte utforme bevis manuelt. Dermed var metoden begrenset til en håndfull kritiske systemer. Selskapet sa at AI nå gjør arbeidet med formelle bevis minst 100 ganger raskere, og at teknologien deres for automatisering av bevisføring øker hastigheten ytterligere 100 ganger, slik at generering av bevis går fra år eller måneder til timer eller minutter.

Selskapet beskrev også teknologien det kaller «spesifikasjonsfabrikken», som ifølge selskapet gjør det mulig for bedrifter og utviklere å omsette menneskelige intensjoner og forretningskrav til presise formelle spesifikasjoner i stor skala. Resultatet er garantier som kan kontrolleres uavhengig, i stedet for å bygge på testing eller påstander fra leverandører.

&Truth bygger på Lean, et åpen kildekode-basert bevissystem, og Mathlib, et bibliotek med mer enn to millioner linjer med matematiske definisjoner og teoremer, i tillegg til åpen kildekode-teknologi som CSLib. Ifølge selskapet er målet å etablere et universelt formelt vokabular for programvare: matematiske modeller av programmeringsspråk og systemer, bevisteknikker og presise spesifikasjoner som muliggjør automatisert verifikasjon på tvers av språk. &Truth sa at selskapet samarbeider med Lean Focused Research Organization og har til hensikt å gjøre grunnlagsbibliotekene sine tilgjengelige som åpen kildekode.

Medgrunnlegger og medadministrerende direktør Clark Barrett sa at Lean og Mathlib ga AI et presist språk for matematisk resonnering, og at programvare har manglet et tilsvarende fundament. Medgrunnlegger og vitenskapelig sjef Ilya Sergey sa at tillit til programvare bør bygge på bevis som kan kontrolleres uavhengig, ikke på ord fra et selskap.

Grunnleggere og to hovedkontorer

Barrett er Corbel-professor i informatikk ved Stanford University, grunnleggende meddirektør for Stanford Center for AI Safety, direktør for Stanford Center for Automated Reasoning, medskaper av CSLib og prosjektleder for den automatiserte resonneringsmotoren cvc5. Sergey grunnla VERSE Lab ved National University of Singapore og var med på å utvikle verifikasjonsverktøyene Veil og Velvet med åpen kildekode. Medgrunnlegger, medadministrerende direktør og styreleder Chris Hsu er medlem av Lean FROs strategiske rådgivningsråd og president for Infinitude Foundation. Tidligere var han administrerende direktør i Kilometre Capital og managing director i Citadel Investment Group.

Kunngjøringen trakk også fram Gregory Malecha, som tidligere ledet arbeidet med formelle metoder i BlueRock Security og var en sentral arkitekt bak verifikasjonsrammeverket BRiCk; Sebastian Ullrich, medarkitekt bak Lean 4 og medgrunnlegger av Lean Focused Research Organization; Linus Lee, tidligere managing partner i Kilometre Capital; og Drew Harman, tidligere kommersiell direktør i Fastino Labs og operativ partner i Insight Partners og Shasta Ventures. &Truth sa at selskapet bygger videre på flere tiår med forskning på formell verifikasjon og automatisert resonnering ved Stanford University og National University of Singapore.

&Truths hovedkontor i USA ligger i Palo Alto, mens det internasjonale hovedkontoret ligger i Singapore. Selskapet sa at kontoret der vil bli betydelig utvidet innen forskning, ingeniørvirksomhet, produktutvikling og markedsintroduksjon. Low Jin Yong, senior visepresident og medleder for Digital Industry Singapore, sa i kunngjøringen at hovedkontoret vil styrke Singapores kompetanse innen tillit og sikkerhet og bidra til å gjøre landet til et bedre utgangspunkt for selskaper som utvikler pålitelig AI.

På selskapets nettsted finner man også en rundebordsdiskusjon med Leonardo de Moura, oppfinneren av Lean og visepresident og fremragende forsker hos AWS, og Simone Severini, medlem av Lean FROs strategiske rådgivningsråd og fremragende ingeniør hos Google.

Følgeartikler utdyper selskapets begrunnelse

I en følgeartikkel datert 29. oktober 2026 beskrev Hsu utviklingstrekkene som ifølge selskapet gjør verifikasjon presserende. Han viste til uttalelser fra Google-sjef Sundar Pichai om at 75 % av ny kode hos Google nå genereres av AI og godkjennes av ingeniører, og til Veracodes testing i 2026, som viste at AI-modeller mislyktes med nesten halvparten av kodeoppgavene der sikkerhet var viktig. Artikkelen viser også til en kampanje i september 2026 der en angriper brukte hundrevis av AI-agenter til å bryte seg inn i 395 organisasjoner i 48 land ved å utnytte sårbarheter i mye brukt programvare for utskriftsadministrasjon. Den omtaler dessuten et rekordhøyt antall på 14 959 programvaresårbarheter publisert i september 2026, et tall som ifølge artikkelen er 3,5 ganger så høyt som antallet som ble publisert året før.

Essayet forteller om tidligere milepæler innen formell verifikasjon: Det opprinnelige beviset for mikrokjernen seL4 krevde omtrent 20 personår med ekspertarbeid for rundt 8 700 kodelinjer; i 2015 ble seL4, under DARPA-programmet HACMS, integrert i Boeings helikopter Unmanned Little Bird, og et profesjonelt red team klarte ikke å trenge gjennom flykontrollene, selv med ukers tilgang; og i september 2026 formaliserte en AI-modell utviklet av Anthropic det fullstendige beviset for Fermats siste teorem i Lean på 11 dager. Essayet påpeker også at Kim Morrison, senior programvareingeniør innen forskning ved Lean FRO, tidligere i 2026 brukte Claude fra Anthropic med minimal menneskelig veiledning til å lage en Lean-versjon av zlib-komprimeringsbiblioteket og bevise at det alltid gjenoppretter nøyaktig de dataene det komprimerte.

Essayet siterer Lean-skaperen Leonardo de Moura: «Testing gir tillit. Bevis gir en garanti.»

I et annet essay publisert 29. oktober 2026 forklarer Sergey hvordan programverifikasjon fungerer. Han tar utgangspunkt i Alan Turings artikkel «Checking a Large Routine» fra 1949, som foreslo at programmerere skulle føye presise påstander til koden sin, slik at en kontrollør kunne verifisere dem enkeltvis. Essayet beskriver spesifikasjoner, løkkeinvarianter og bevis kontrollert i Lean, og sier at målet til &Truth er at utviklere skal kunne få uavhengig kontrollerbare bevis, for eksempel et formelt bevis i Lean, til en kostnad som gjør verifikasjon til en rutinemessig del av utviklingen.

&Truth beskriver sin langsiktige visjon som en overgang fra «vibbekoding» til «verifiseringskoding», der AI-generert kode verifiseres matematisk før utrulling, AI-agenter opererer i miljøer med beviselig avgrensede rammer, eldre programvare moderniseres på en trygg måte, og kritisk infrastruktur beskyttes av matematisk dokumentasjon som kan kontrolleres uavhengig.