&Truth strânge 70 de milioane de dolari într-o rundă seed pentru a construi o mașină universală de verificare a codului

&Truth, o societate de interes public care dezvoltă tehnologii pentru a demonstra matematic siguranța software-ului, a ieșit din stealth pe 29 octombrie 2026, anunțând o finanțare seed de 70 de milioane de dolari și planul de a construi ceea ce numește o mașină universală de verificare a codului.

În anunțul lansării, compania a declarat că a fost fondată la începutul anului 2026 și a primit 70 de milioane de dolari în capital seed de la un grup pe care l-a descris drept format din lideri de referință în domeniul siguranței IA și al capitalului de risc. Compania a spus că mașina sa de verificare este concepută să citească cod în orice limbaj de programare și să demonstreze matematic că acesta este sigur, securizat și corect, prin demonstrații pe care oricine le poate verifica independent.

Automatizarea demonstrațiilor, construită pe Lean

Verificarea formală există de zeci de ani, dar până acum a fost inaccesibilă și costisitoare, se arată în anunț, deoarece experții trebuiau să formuleze manual demonstrațiile, ceea ce limita practica la un număr restrâns de sisteme critice. Compania a spus că IA accelerează acum lucrul la demonstrațiile formale de cel puțin 100 de ori, iar tehnologia sa de automatizare a demonstrațiilor accelerează procesul de încă 100 de ori, reducând timpul necesar generării unei demonstrații de la ani sau luni la ore sau minute.

Compania a prezentat și tehnologia pe care o numește „fabrică de specificații”, despre care a spus că le permite întreprinderilor și dezvoltatorilor să transforme intențiile oamenilor și cerințele de afaceri în specificații formale precise, la scară largă, oferind garanții care pot fi verificate independent, în loc să se bazeze pe testare sau pe afirmațiile furnizorilor.

&Truth își construiește tehnologia pe Lean, un sistem de demonstrații cu sursă deschisă, și pe Mathlib, o bibliotecă cu peste două milioane de linii de definiții și teoreme matematice, precum și pe tehnologii cu sursă deschisă, inclusiv CSLib. Potrivit companiei, obiectivul este crearea unui vocabular formal universal pentru software: modele matematice ale limbajelor de programare și ale sistemelor, tehnici de demonstrație și specificații precise care permit verificarea automată în diferite limbaje. &Truth a declarat că lucrează cu Lean Focused Research Organization și că intenționează să publice bibliotecile sale fundamentale cu sursă deschisă.

Co-fondatorul și co-directorul general Clark Barrett a spus că Lean și Mathlib au oferit IA un limbaj precis pentru raționamentul matematic, dar că software-ului i-a lipsit o bază echivalentă. Co-fondatorul și directorul științific Ilya Sergey a spus că încrederea în software ar trebui să se bazeze pe demonstrații verificabile independent, nu pe cuvântul vreunei companii.

Fondatorii și sediile centrale din două țări

Barrett este profesor Corbel de informatică la Stanford University, codirector fondator al Stanford Center for AI Safety, director al Stanford Center for Automated Reasoning, co-creator al CSLib și coordonator de proiect pentru motorul de raționament automat cvc5. Sergey a fondat VERSE Lab la National University of Singapore și a creat împreună cu alții verificatoarele cu sursă deschisă Veil și Velvet. Co-fondatorul, co-directorul general și președintele executiv Chris Hsu este membru al consiliului consultativ strategic Lean FRO și președintele Infinitude Foundation; anterior, a fost director general al Kilometre Capital și director general la Citadel Investment Group.

Anunțul i-a menționat și pe Gregory Malecha, care a condus anterior activitatea în domeniul metodelor formale la BlueRock Security și a fost unul dintre arhitecții principali ai cadrului de verificare BRiCk; Sebastian Ullrich, co-arhitect al Lean 4 și cofondator al Lean Focused Research Organization; Linus Lee, fost partener director la Kilometre Capital; și Drew Harman, fost director comercial la Fastino Labs și partener operațional la Insight Partners și Shasta Ventures. &Truth a spus că activitatea sa se bazează pe zeci de ani de cercetare în verificarea formală și raționamentul automat desfășurată la Stanford University și National University of Singapore.

Sediul central al &Truth din SUA este în Palo Alto, iar sediul său internațional este în Singapore, unde, potrivit companiei, biroul se va extinde semnificativ în domeniile cercetării, ingineriei, produsului și dezvoltării comerciale. Low Jin Yong, vicepreședinte senior și codirector al Digital Industry Singapore, a declarat în anunț că sediul central va consolida capacitățile Singapore în materie de încredere și siguranță și va întări poziția țării ca bază pentru companiile care dezvoltă IA de încredere.

Site-ul companiei prezintă și o discuție la masă rotundă cu Leonardo de Moura, inventatorul Lean și vicepreședinte și cercetător distins la AWS, și Simone Severini, membru al consiliului consultativ strategic Lean FRO și inginer distins la Google.

Eseurile care însoțesc anunțul explică rațiunile companiei

În un eseu însoțitor din 29 octombrie 2026, Hsu a detaliat tendințele care, potrivit companiei, fac urgentă verificarea, citând declarația directorului general al Google, Sundar Pichai, potrivit căreia 75% din codul nou de la Google este generat acum de IA și aprobat de ingineri, precum și testarea realizată de Veracode în 2026, care a constatat că modelele de IA au eșuat la aproape jumătate dintre sarcinile de programare în care securitatea era importantă. Eseul menționează și o campanie din septembrie 2026, în cadrul căreia un atacator a folosit sute de agenți IA pentru a compromite 395 de organizații din 48 de țări, exploatând vulnerabilități dintr-un software de gestionare a imprimării utilizat pe scară largă, precum și un număr record de 14.959 de vulnerabilități software publicate în septembrie 2026, cifră pe care o descrie ca fiind de 3,5 ori mai mare decât numărul publicat cu un an înainte.

Eseul trece în revistă repere anterioare din verificarea formală: demonstrația inițială pentru microkernelul seL4 a necesitat aproximativ 20 de ani-persoană de muncă din partea unor experți, pentru circa 8.700 de linii de cod; în 2015, în cadrul programului HACMS al DARPA, seL4 a fost integrat în elicopterul Unmanned Little Bird al Boeing, ale cărui comenzi de zbor nu au putut fi compromise de o echipă red team profesionistă, deși aceasta a avut acces timp de câteva săptămâni; iar în septembrie 2026, un model de inteligență artificială dezvoltat de Anthropic a formalizat în Lean demonstrația completă a ultimei teoreme a lui Fermat în 11 zile. Eseul mai menționează că, la începutul anului 2026, Kim Morrison, inginer software de cercetare cu rang senior la Lean FRO, a folosit Claude de la Anthropic, cu îndrumare umană minimă, pentru a crea o versiune Lean a bibliotecii de compresie zlib și a demonstra că aceasta restituie întotdeauna exact datele pe care le-a comprimat.

Eseul îl citează pe Leonardo de Moura, creatorul Lean: „Testarea oferă încredere. Demonstrația oferă o garanție.”

În un al doilea eseu, publicat la 29 octombrie 2026, Sergey explică mecanismele verificării programelor, pornind de la lucrarea lui Alan Turing din 1949, „Checking a Large Routine”, în care acesta propunea ca programatorii să-și însoțească codul de afirmații precise, pe care un verificator să le poată verifica individual. Eseul descrie specificațiile, invarianții buclelor și demonstrațiile verificate în Lean și precizează că obiectivul &Truth este ca dezvoltatorii să obțină dovezi verificabile independent, precum o demonstrație formală în Lean, la un cost care să facă din verificare o etapă obișnuită a procesului de dezvoltare.

&Truth își descrie viziunea pe termen lung ca pe o trecere de la „programarea intuitivă” la „programarea verificată”, în care codul generat de inteligența artificială este verificat matematic înainte de implementare, agenții de inteligență artificială operează în medii a căror izolare poate fi demonstrată formal, software-ul învechit este modernizat în siguranță, iar infrastructura critică este protejată prin garanții matematice verificabile independent.