&Truth kerää 70 miljoonaa dollaria siemenrahoitusta rakentaakseen yleiskäyttöisen koodin verifiointikoneen

Ohjelmistojen turvallisuuden matemaattiseen todistamiseen tarkoitettua teknologiaa kehittävä yleishyödyllinen yhtiö &Truth astui esiin piilosta 29. lokakuuta 2026. Yhtiö kertoi keränneensä 70 miljoonaa dollaria siemenrahoitusta ja aikovansa rakentaa sen, mitä se kutsuu yleiskäyttöiseksi koodin verifiointikoneeksi.

Yhtiö kertoi julkistamisilmoituksessaan, että se perustettiin vuoden 2026 alussa ja että se sai 70 miljoonan dollarin siemenrahoituksen ryhmältä, jota se kuvaili tekoälyn turvallisuuden ja pääomasijoittamisen suunnannäyttäjiksi. Yhtiön mukaan sen verifiointikonetta kehitetään lukemaan minkä tahansa ohjelmointikielen koodia ja todistamaan matemaattisesti, että koodi on turvallista, tietoturvallista ja oikein toimivaa. Todistukset ovat kenen tahansa itsenäisesti tarkistettavissa.

Todistusten automatisointi Lean-järjestelmän pohjalta

Muodollista verifiointia on tehty vuosikymmeniä, mutta se oli aiemmin vaikeasti saavutettavaa ja kallista, yhtiö kertoi ilmoituksessaan. Asiantuntijoiden täytyi muodostaa todistukset käsin, minkä vuoksi menetelmää voitiin käyttää vain muutamissa kriittisissä järjestelmissä. Yhtiön mukaan tekoäly nopeuttaa nykyään muodollisten todistusten laatimista vähintään satakertaisesti, ja sen todistusten automatisointiteknologia nopeuttaa prosessia vielä toiset sata kertaa. Näin todistusten tuottamiseen aiemmin kuluneista vuosista tai kuukausista selvitään tunneissa tai minuuteissa.

Yhtiö kuvaili myös niin sanottua ”spesifikaatiotehdas”-teknologiaansa, jonka se kertoi auttavan yrityksiä ja kehittäjiä muuntamaan ihmisten tavoitteet ja liiketoiminnan vaatimukset täsmällisiksi muodollisiksi spesifikaatioiksi suuressa mittakaavassa. Näin syntyvät takuut voidaan tarkistaa itsenäisesti, eivätkä ne perustu testaukseen tai toimittajien väitteisiin.

&Truth rakentaa avoimen lähdekoodin todistusjärjestelmän Lean ja Mathlibin varaan. Mathlib on kirjasto, joka sisältää yli kaksi miljoonaa riviä matemaattisia määritelmiä ja lauseita. Lisäksi yhtiö hyödyntää avoimen lähdekoodin teknologioita, kuten CSLib-kirjastoa. Yhtiön tavoitteena on luoda ohjelmistoille yleiskäyttöinen muodollinen sanasto: ohjelmointikielten ja järjestelmien matemaattisia malleja, todistustekniikoita sekä täsmällisiä spesifikaatioita, jotka mahdollistavat automaattisen verifioinnin eri ohjelmointikielillä. &Truth kertoi tekevänsä yhteistyötä Lean Focused Research Organizationin kanssa ja aikovansa julkaista perustavanlaatuiset kirjastonsa avoimena lähdekoodina.

Perustaja ja toimitusjohtaja Clark Barrett sanoi, että Lean ja Mathlib tarjoavat tekoälylle täsmällisen kielen matemaattiseen päättelyyn, mutta ohjelmistoilta on puuttunut vastaava perusta. Perustaja ja tieteellinen johtaja Ilya Sergey sanoi, että luottamuksen ohjelmistoihin pitäisi perustua itsenäisesti tarkistettavissa oleviin todistuksiin, ei minkään yrityksen sanaan.

Perustajat ja kaksi päätoimipaikkaa

Barrett on tietojenkäsittelytieteen Corbel-professori Stanford Universityssä, Stanford Center for AI Safetyn perustajajäsen ja toinen johtaja, Stanford Center for Automated Reasoningin johtaja, CSLib-kirjaston toinen luoja sekä automaattisen päättelyn cvc5-moottorin projektijohtaja. Sergey perusti VERSE Labin National University of Singaporeen ja oli mukana luomassa avoimen lähdekoodin verifiointityökaluja Veil ja Velvet. Perustaja, toimitusjohtaja ja hallituksen puheenjohtaja Chris Hsu kuuluu Lean FRO Strategic Advisory Boardiin ja johtaa Infinitude Foundationia. Aiemmin hän toimi Kilometre Capitalin toimitusjohtajana ja Citadel Investment Groupin toimitusjohtajana.

Ilmoituksessa mainittiin myös Gregory Malecha, joka johti aiemmin muodollisten menetelmien kehitystä BlueRock Securityssä ja oli BRiCk-verifiointikehyksen keskeinen arkkitehti; Sebastian Ullrich, Lean 4:n toinen arkkitehti ja Lean Focused Research Organizationin perustajajäsen; Linus Lee, Kilometre Capitalin entinen johtava osakas; sekä Drew Harman, Fastino Labsin entinen kaupallinen johtaja ja Insight Partnersin ja Shasta Venturesin toimiva osakas. &Truth kertoi rakentavansa Stanford Universityn ja National University of Singaporen vuosikymmenten muodollisen verifioinnin ja automaattisen päättelyn tutkimuksen pohjalta.

&Truthin Yhdysvaltain päätoimipaikka sijaitsee Palo Altossa ja kansainvälinen päätoimipaikka Singaporessa. Yhtiön mukaan sen toimisto Singaporessa laajenee merkittävästi tutkimuksen, suunnittelun, tuotekehityksen ja kaupallisen toiminnan aloilla. Singaporen digitaalisen teollisuuden varajohtaja ja toinen johtaja Low Jin Yong sanoi ilmoituksessa, että päätoimipaikka syventää Singaporen luottamukseen ja turvallisuuteen liittyvää osaamista ja vahvistaa maan asemaa luotettavaa tekoälyä kehittävien yritysten tukikohtana.

Yhtiön verkkosivuilla on myös pyöreän pöydän keskustelu, johon osallistuvat Lean-järjestelmän kehittäjä ja AWS:n varatoimitusjohtaja sekä arvostettu tutkija Leonardo de Moura ja Lean FRO Strategic Advisory Boardin jäsen sekä Googlen arvostettu insinööri Simone Severini.

Tausta-artikkelit avaavat yhtiön perusteluja

Hsu käsitteli yhtiön mukaan verifioinnista kiireellistä tekeviä kehityssuuntia tausta-artikkelissa, joka julkaistiin 29. lokakuuta 2026. Hän viittasi Googlen toimitusjohtajan Sundar Pichain lausuntoon, jonka mukaan tekoäly tuottaa nykyään 75 % Googlen uudesta koodista ja insinöörit hyväksyvät sen, sekä Veracoden vuoden 2026 testaukseen. Siinä tekoälymallit epäonnistuivat lähes puolessa niistä koodaustehtävistä, joissa tietoturvalla oli merkitystä. Artikkelissa mainitaan myös syyskuussa 2026 toteutettu kampanja, jossa hyökkääjä käytti satoja tekoälyagentteja murtautuakseen 395 organisaatioon 48 maassa yleisesti käytetyn tulostuksenhallintaohjelmiston haavoittuvuuksien kautta, sekä syyskuussa 2026 julkaistut ennätykselliset 14 959 ohjelmistohaavoittuvuutta. Artikkelin mukaan määrä oli 3,5-kertainen vuotta aiemmin julkaistuihin haavoittuvuuksiin verrattuna.

Esseessä käydään läpi aiempia muodollisen verifioinnin merkkipaaluja: seL4-mikroytimen alkuperäisen todistuksen tekeminen vaati noin 20 henkilötyövuotta asiantuntijatyötä noin 8 700 koodiriville; vuonna 2015 seL4 sisällytettiin DARPA:n HACMS-ohjelmassa Boeingin Unmanned Little Bird -helikopteriin, jonka lennonohjausjärjestelmää ammattilaisista koostunut punatiimi ei pystynyt murtamaan, vaikka sillä oli viikkoja aikaa; ja syyskuussa 2026 Anthropicin kehittämä tekoälymalli muodollisti Leanissa Fermat’n viimeisen lauseen täydellisen todistuksen 11 päivässä. Esseessä todetaan myös, että aiemmin vuonna 2026 Lean FRO:n johtava tutkimusohjelmistosuunnittelija Kim Morrison käytti Anthropicin Claudea vähäisellä ihmisen ohjauksella rakentaakseen Lean-version zlib-pakkauskirjastosta ja todistaakseen, että se palauttaa aina täsmälleen pakkaamansa tiedot.

Esseessä lainataan Leanin luojaa Leonardo de Mouraa: ”Testaus antaa luottamusta. Todistus antaa takuun.”

Toisessa 29. lokakuuta 2026 julkaistussa esseessä Sergey selittää ohjelmien verifioinnin toimintaperiaatteita ja aloittaa Alan Turingin vuonna 1949 julkaisemasta artikkelista ”Checking a Large Routine”, jossa ehdotettiin, että ohjelmoijat esittäisivät koodinsa yhteydessä täsmällisiä väitteitä, jotka tarkistin voisi todentaa yksitellen. Esseessä käsitellään määrittelyjä, silmukkainvariantteja ja Leanissa tarkistettavia todistuksia. Siinä todetaan, että &Truthin tavoitteena on, että kehittäjät voivat saada itsenäisesti tarkistettavaa näyttöä, kuten Leanissa laaditun muodollisen todistuksen, sellaisin kustannuksin, että verifioinnista tulee ohjelmistokehityksen tavanomainen osa.

&Truth kuvaa pitkän aikavälin visiotaan siirtymänä ”fiiliskoodauksesta” ”todennuskoodaukseen”: tekoälyn tuottama koodi todennetaan matemaattisesti ennen käyttöönottoa, tekoälyagentit toimivat ympäristöissä, joiden eristys voidaan todistaa, vanhaa ohjelmistoa uudistetaan turvallisesti ja kriittistä infrastruktuuria suojataan itsenäisesti tarkistettavilla matemaattisilla takuilla.