&Truth raccoglie 70 milioni di dollari in un round seed per creare una macchina universale di verifica del codice

&Truth, una società di pubblica utilità che sviluppa tecnologie per dimostrare matematicamente la sicurezza del software, è uscita dalla fase stealth il 29 ottobre 2026, annunciando un finanziamento seed di 70 milioni di dollari e il progetto di realizzare quella che definisce una macchina universale per la verifica del codice.

Nel comunicato di lancio, la società ha dichiarato di essere stata fondata all’inizio del 2026 e di aver raccolto 70 milioni di dollari in capitale seed da un gruppo di figure di spicco che hanno contribuito a plasmare i settori della sicurezza dell’IA e del venture capital. La società ha spiegato che la sua macchina di verifica è in fase di sviluppo per leggere codice scritto in qualsiasi linguaggio di programmazione e dimostrare matematicamente che è sicuro, protetto e corretto, con dimostrazioni che chiunque può verificare in modo indipendente.

Automazione delle dimostrazioni basata su Lean

Secondo il comunicato, la verifica formale esiste da decenni, ma in precedenza era inaccessibile e costosa: gli esperti dovevano formulare manualmente le dimostrazioni, limitando questa pratica a pochi sistemi critici. La società ha affermato che oggi l’IA accelera di 100 volte o più il lavoro sulle dimostrazioni formali e che la sua tecnologia di automazione delle dimostrazioni velocizza il processo di un ulteriore fattore 100, riducendo i tempi necessari per generarle da anni o mesi a ore o minuti.

La società ha inoltre descritto quella che definisce una tecnologia di «fabbrica di specifiche», che, a suo dire, consente alle aziende e agli sviluppatori di tradurre su larga scala le intenzioni umane e i requisiti aziendali in specifiche formali precise, producendo garanzie verificabili in modo indipendente anziché basate sui test o sulle dichiarazioni dei fornitori.

&Truth si basa su Lean, un sistema open source per le dimostrazioni, e Mathlib, una libreria con oltre due milioni di righe di definizioni e teoremi matematici, oltre che su tecnologie open source come CSLib. Secondo la società, l’obiettivo è creare un vocabolario formale universale per il software: modelli matematici dei linguaggi di programmazione e dei sistemi, tecniche di dimostrazione e specifiche precise che consentano la verifica automatizzata in diversi linguaggi. &Truth ha dichiarato di collaborare con la Lean Focused Research Organization e di voler rilasciare le proprie librerie fondamentali come software open source.

Clark Barrett, cofondatore e co-CEO, ha affermato che Lean e Mathlib hanno fornito all’IA un linguaggio preciso per ragionare in matematica, mentre al software è mancata una base equivalente. Ilya Sergey, cofondatore e direttore scientifico, ha dichiarato che la fiducia nel software dovrebbe fondarsi su dimostrazioni verificabili in modo indipendente, non sulle parole di un’azienda.

Fondatori e sedi principali

Barrett è titolare della cattedra Corbel di informatica presso Stanford University, co-direttore fondatore dello Stanford Center for AI Safety, direttore dello Stanford Center for Automated Reasoning, co-creatore di CSLib e responsabile del progetto del motore di ragionamento automatizzato cvc5. Sergey ha fondato il VERSE Lab presso la National University of Singapore e ha co-creato i verificatori open source Veil e Velvet. Chris Hsu, cofondatore, co-CEO e presidente esecutivo, fa parte del Lean FRO Strategic Advisory Board ed è presidente della Infinitude Foundation; in precedenza è stato CEO di Kilometre Capital e direttore di Citadel Investment Group.

Il comunicato ha inoltre citato Gregory Malecha, che in precedenza ha diretto le attività sui metodi formali presso BlueRock Security ed è stato uno dei principali architetti del framework di verifica BRiCk; Sebastian Ullrich, co-progettista di Lean 4 e cofondatore della Lean Focused Research Organization; Linus Lee, già managing partner di Kilometre Capital; e Drew Harman, già direttore commerciale di Fastino Labs e operating partner presso Insight Partners e Shasta Ventures. &Truth ha dichiarato di basarsi su decenni di ricerca sulla verifica formale e sul ragionamento automatizzato condotta presso Stanford University e la National University of Singapore.

La sede statunitense di &Truth è a Palo Alto, mentre quella internazionale si trova a Singapore, dove, secondo la società, l’ufficio si amplierà notevolmente nelle aree della ricerca, dell’ingegneria, dello sviluppo dei prodotti e delle attività commerciali. Nel comunicato, Low Jin Yong, vicepresidente senior e co-responsabile di Digital Industry Singapore, ha dichiarato che la sede rafforzerà le capacità di Singapore in materia di fiducia e sicurezza e consoliderà il ruolo del Paese come base per le aziende che sviluppano IA affidabile.

Il sito web della società presenta anche una discussione a tavola rotonda con Leonardo de Moura, inventore di Lean e vicepresidente e Distinguished Scientist presso AWS, e Simone Severini, membro del Lean FRO Strategic Advisory Board e Distinguished Engineer presso Google.

Saggi di approfondimento illustrano le motivazioni della società

In un saggio di approfondimento del 29 ottobre 2026, Hsu ha illustrato le tendenze che, secondo la società, rendono urgente la verifica. Ha citato le dichiarazioni dell’amministratore delegato di Google, Sundar Pichai, secondo cui oggi il 75% del nuovo codice di Google è generato dall’IA e approvato dagli ingegneri, e i test condotti da Veracode nel 2026, che hanno rilevato come i modelli di IA fallissero in quasi la metà delle attività di programmazione in cui la sicurezza era importante. Il saggio cita inoltre una campagna del settembre 2026 durante la quale un aggressore ha impiegato centinaia di agenti di IA per violare 395 organizzazioni in 48 Paesi, sfruttando vulnerabilità in un software di gestione della stampa ampiamente utilizzato, e il numero record di 14.959 vulnerabilità software pubblicate nel settembre 2026, una cifra che, secondo il saggio, è 3,5 volte superiore a quella dell’anno precedente.

Il saggio ripercorre alcune tappe precedenti della verifica formale: la dimostrazione originale del microkernel seL4 richiese circa 20 anni-persona di lavoro specialistico per circa 8.700 righe di codice; nel 2015, nell’ambito del programma HACMS della DARPA, seL4 fu integrato nell’elicottero Unmanned Little Bird di Boeing, i cui comandi di volo non poterono essere violati da una squadra di red team professionisti, pur avendo avuto settimane per tentare l’attacco; e, nel settembre 2026, un modello di IA sviluppato da Anthropic formalizzò in Lean la dimostrazione completa dell’ultimo teorema di Fermat in 11 giorni. Il saggio osserva inoltre che, all’inizio del 2026, Kim Morrison, ingegnere senior del software di ricerca presso il Lean FRO, utilizzò Claude di Anthropic con una guida umana minima per realizzare una versione in Lean della libreria di compressione zlib e dimostrare che ripristina sempre esattamente i dati che ha compresso.

Il saggio cita il creatore di Lean, Leonardo de Moura: «I test danno fiducia. Le dimostrazioni offrono una garanzia».

In un secondo saggio pubblicato il 29 ottobre 2026, Sergey spiega i meccanismi della verifica dei programmi, partendo dall’articolo del 1949 di Alan Turing, «Checking a Large Routine», in cui si proponeva che i programmatori accompagnassero il codice con affermazioni precise, verificabili singolarmente da un sistema di controllo. Il saggio illustra le specifiche, gli invarianti dei cicli e le dimostrazioni verificate in Lean, e afferma che l’obiettivo di &Truth è consentire agli sviluppatori di ottenere prove verificabili in modo indipendente, come una dimostrazione formale in Lean, a un costo tale da rendere la verifica una parte ordinaria dello sviluppo.

&Truth descrive la propria visione a lungo termine come un passaggio dalla «programmazione a intuito» alla «programmazione verificata»: il codice generato dall’IA viene verificato matematicamente prima della distribuzione, gli agenti IA operano in ambienti il cui confinamento è dimostrabile, il software legacy viene modernizzato in sicurezza e le infrastrutture critiche sono protette da garanzie matematiche verificabili in modo indipendente.