&Truth pozyskuje 70 mln USD w rundzie zalążkowej na budowę uniwersalnej maszyny do weryfikacji kodu

&Truth, spółka pożytku publicznego opracowująca technologie służące do matematycznego dowodzenia, że oprogramowanie jest bezpieczne, wyszła z ukrycia 29 października 2026 r. i poinformowała o pozyskaniu 70 mln USD finansowania zalążkowego oraz planie budowy tego, co nazywa uniwersalną maszyną do weryfikacji kodu.

W ogłoszeniu o rozpoczęciu działalności firma poinformowała, że powstała na początku 2026 r. i pozyskała 70 mln USD kapitału zalążkowego od grupy osób, które określiła jako czołowych przedstawicieli bezpieczeństwa AI i rynku venture capital. Firma podała, że buduje maszynę weryfikacyjną, która ma odczytywać kod w dowolnym języku programowania i matematycznie dowodzić, że jest on bezpieczny, odporny na zagrożenia i poprawny, a każdy będzie mógł niezależnie sprawdzić te dowody.

Automatyzacja dowodzenia oparta na Lean

Jak podano w ogłoszeniu, weryfikacja formalna istnieje od dziesięcioleci, ale wcześniej była niedostępna i kosztowna, ponieważ eksperci musieli ręcznie formułować dowody, co ograniczało jej zastosowanie do garstki systemów o krytycznym znaczeniu. Firma stwierdziła, że AI przyspiesza obecnie prace nad dowodami formalnymi co najmniej 100-krotnie, a jej technologia automatyzacji dowodzenia przyspiesza ten proces o kolejne 100 razy, skracając czas tworzenia dowodów z lat lub miesięcy do godzin lub minut.

Firma opisała również technologię, którą nazywa „fabryką specyfikacji”. Według niej umożliwia ona przedsiębiorstwom i programistom przekładanie ludzkich intencji i wymagań biznesowych na precyzyjne specyfikacje formalne na dużą skalę, zapewniając gwarancje, które można niezależnie sprawdzić, zamiast opierać się na testach lub deklaracjach dostawców.

&Truth rozwija rozwiązania oparte na Lean, systemie dowodzenia z otwartym kodem źródłowym, oraz Mathlib — bibliotece zawierającej ponad dwa miliony wierszy definicji matematycznych i twierdzeń — a także na technologiach open source, w tym CSLib. Według firmy celem jest stworzenie uniwersalnego języka formalnego dla oprogramowania: modeli matematycznych języków programowania i systemów, technik dowodzenia oraz precyzyjnych specyfikacji, które umożliwią automatyczną weryfikację w różnych językach. &Truth poinformowała, że współpracuje z Lean Focused Research Organization i zamierza udostępnić swoje podstawowe biblioteki na zasadach open source.

Współzałożyciel i współprezes Clark Barrett powiedział, że Lean i Mathlib zapewniły AI precyzyjny język do rozumowania matematycznego, natomiast w oprogramowaniu brakowało równoważnego fundamentu. Współzałożyciel i dyrektor ds. naukowych Ilya Sergey stwierdził, że zaufanie do oprogramowania powinno opierać się na dowodach, które można niezależnie sprawdzić, a nie na słowach jakiejkolwiek firmy.

Założyciele i dwie siedziby główne

Barrett jest profesorem informatyki na katedrze Corbel na Stanford University, współzałożycielem i współdyrektorem Stanford Center for AI Safety, dyrektorem Stanford Center for Automated Reasoning, współtwórcą CSLib oraz kierownikiem projektu silnika automatycznego wnioskowania cvc5. Sergey założył VERSE Lab na National University of Singapore i współtworzył weryfikatory open source Veil i Velvet. Współzałożyciel, współprezes i prezes wykonawczy Chris Hsu zasiada w radzie doradczej Lean FRO i kieruje Infinitude Foundation; wcześniej był dyrektorem generalnym Kilometre Capital oraz dyrektorem zarządzającym Citadel Investment Group.

W ogłoszeniu wymieniono również Gregory’ego Malechę, który wcześniej kierował zespołem metod formalnych w BlueRock Security i był jednym z głównych architektów platformy weryfikacyjnej BRiCk; Sebastiana Ullricha, współarchitekta Lean 4 i współzałożyciela Lean Focused Research Organization; Linusa Lee, byłego partnera zarządzającego w Kilometre Capital; oraz Drew Harmana, byłego dyrektora handlowego w Fastino Labs i partnera operacyjnego w Insight Partners i Shasta Ventures. &Truth poinformowała, że rozwija rozwiązania w oparciu o wieloletnie badania nad weryfikacją formalną i automatycznym wnioskowaniem prowadzone na Stanford University i National University of Singapore.

Siedziba główna &Truth w Stanach Zjednoczonych mieści się w Palo Alto, a jej międzynarodowa siedziba — w Singapurze. Firma poinformowała, że singapurskie biuro znacznie rozszerzy działalność w obszarach badań, inżynierii, rozwoju produktów i komercjalizacji. Low Jin Yong, starszy wiceprezes i współkierownik Digital Industry Singapore, powiedział w ogłoszeniu, że siedziba pogłębi kompetencje Singapuru w zakresie zaufania i bezpieczeństwa oraz umocni pozycję kraju jako miejsca, z którego firmy rozwijają godną zaufania AI.

Na stronie internetowej firmy można również znaleźć dyskusję przy okrągłym stole z Leonardem de Mourą, twórcą Lean oraz wiceprezesem i wybitnym naukowcem w AWS, a także Simone Severini, członkinią rady doradczej Lean FRO i wybitną inżynierką w Google.

Eseje uzupełniające wyjaśniają motywacje firmy

W eseju uzupełniającym z 29 października 2026 r. Hsu omówił trendy, które — jak twierdzi firma — sprawiają, że weryfikacja staje się pilna. Przytoczył wypowiedź Sundara Pichai, dyrektora generalnego Google, że 75% nowego kodu w Google jest obecnie generowane przez AI i zatwierdzane przez inżynierów, a także wyniki testów Veracode z 2026 r., które wykazały, że modele AI nie poradziły sobie z niemal połową zadań programistycznych, w których bezpieczeństwo miało znaczenie. W eseju wspomniano również o kampanii z września 2026 r., podczas której napastnik wykorzystał setki agentów AI, by zaatakować 395 organizacji w 48 krajach za pośrednictwem luk w powszechnie używanym oprogramowaniu do zarządzania drukiem, oraz o rekordowej liczbie 14 959 luk w oprogramowaniu opublikowanych we wrześniu 2026 r. — 3,5 raza większej niż liczba opublikowana rok wcześniej.

Esej przypomina wcześniejsze przełomowe osiągnięcia w dziedzinie weryfikacji formalnej: przygotowanie pierwotnego dowodu dla mikrojądra seL4 wymagało około 20 osobolat pracy ekspertów i objęło około 8700 wierszy kodu; w 2015 roku, w ramach programu HACMS DARPA, system seL4 zainstalowano w śmigłowcu Unmanned Little Bird firmy Boeing, a profesjonalny zespół red team, któremu udostępniono jego układy sterowania lotem na kilka tygodni, nie zdołał ich zaatakować; we wrześniu 2026 roku model AI opracowany przez Anthropic sformalizował w Lean pełny dowód wielkiego twierdzenia Fermata w ciągu 11 dni. Esej odnotowuje również, że wcześniej, w 2026 roku, Kim Morrison, starszy inżynier oprogramowania badawczego w Lean FRO, wykorzystał Claude firmy Anthropic, przy minimalnym wsparciu człowieka, do stworzenia wersji biblioteki kompresji zlib w Lean i udowodnienia, że zawsze odtwarza ona dokładnie te dane, które skompresowała.

Esej przytacza słowa twórcy Lean, Leonarda de Moury: „Testowanie daje pewność. Dowód daje gwarancję”.

W drugim eseju opublikowanym 29 października 2026 roku Sergey wyjaśnia mechanizmy weryfikacji programów, zaczynając od artykułu Alana Turinga z 1949 roku „Checking a Large Routine”, w którym zaproponował, by programiści dołączali do kodu precyzyjne twierdzenia, które weryfikator mógłby sprawdzać pojedynczo. Esej opisuje specyfikacje, niezmienniki pętli i dowody sprawdzane w Lean, a także stwierdza, że celem &Truth jest umożliwienie programistom uzyskiwania niezależnie weryfikowalnych dowodów, takich jak formalny dowód w Lean, przy kosztach pozwalających uczynić weryfikację rutynowym elementem procesu programowania.

&Truth opisuje swoją długoterminową wizję jako przejście od „kodowania na wyczucie” do „kodowania z weryfikacją”, w którym kod generowany przez AI jest matematycznie weryfikowany przed wdrożeniem, agenci AI działają w środowiskach, których ograniczone działanie można formalnie udowodnić, starsze oprogramowanie jest bezpiecznie modernizowane, a infrastruktura krytyczna jest chroniona dzięki niezależnie weryfikowalnym gwarancjom matematycznym.