Software · 30 ottobre 2026 · 4 min di lettura
La matematica che blinda il codice: centinaia di milioni di dollari per automatizzare la verifica formale
In sintesi: Per decenni la verifica formale è rimasta un miraggio confinato all'aerospazio e alla crittografia militare per via di costi proibitivi e mesi di lavoro manuale. Ora l'intelligenza artificiale promette di ribaltare il paradigma: la startup &Truth esce allo scoperto con 70 milioni di dollari, affiancando Harmonic e Anthropic nella corsa a trasformare il codice in teoremi matematici verificabili in poche ore. Una svolta che promette di arginare le falle del codice generato da macchine e inaugurare l'era della certezza algoritmica.
di Team Mocchi's
L'illusione dei test e il sogno della prova matematica
Negli ultimi due anni la proliferazione di assistenti di programmazione basati su modelli linguistici ha moltiplicato a dismisura il volume di codice scritto ogni giorno. In parallelo, però, è cresciuto l'allarme per la qualità e la sicurezza dei software rilasciati: persino le suite di testing più capillari, spinte a verificare miliardi di combinazioni, possono soltanto scovare i problemi previsti dagli ingegneri, senza mai certificare l'assenza totale di anomalie o vulnerabilità nascoste.
La risposta teorica a questa debolezza esiste da decenni e risponde al nome di verifica formale. Si tratta di una disciplina che converte le funzioni software e le architetture hardware in proposizioni matematiche formali, impiegando dimostratori di teoremi per provare algebricamente che un programma si comporti esattamente secondo le specifiche in qualsiasi condizione. Finora, questo rigore è rimasto appannaggio quasi esclusivo di progetti critici della NASA o di componenti crittografici per microprocessori, perché tradurre manualmente il codice in formule astratte richiedeva mesi di lavoro di matematici specializzati e budget inaccessibili alle normali aziende tecnologiche.
Dalle librerie di Signal a 500 dollari: la svolta di Stanford
A rompere questo collo di bottiglia è intervenuta la convergenza tra modelli di frontiera e dimostratori formali. Come riporta WIRED, una ricerca condotta da Chuyue Sun e dal suo team all'Università di Stanford ha dimostrato sul campo le potenzialità di questo approccio: un agente basato su intelligenza artificiale è riuscito a verificare e certificare formalmente una porzione critica del codice di cifratura dell'applicazione di messaggistica Signal in meno di mezza giornata, spendendo meno di 500 dollari in calcolo computazionale. Quello stesso compito, svolto precedentemente a mano, aveva impegnato tre tra i massimi esperti mondiali per oltre cinque mesi.
Sulla scia di questi risultati, Sun ha co-fondato la startup &Truth, guidata dal chief science officer Ilya Sergey, che ha annunciato il debutto pubblico con una raccolta di capitali da 70 milioni di dollari. La missione della società è automatizzare la verifica matematica su qualsiasi linguaggio di programmazione mainstream. Sergey traccia un'analogia con l'ingegneria civile: ponti ed edifici non crollano perché i progettisti eseguono calcoli matematici rigorosi prima di gettare le fondamenta; l'industria digitale ha finora rinunciato a questo standard solo per l'impossibilità di scalare il ragionamento formale a costi ragionevoli.
I grandi capitali: la sfida tra Harmonic e l'alleanza Anthropic-Theorem
Il fermento intorno alla formalizzazione automatica ha innescato una vera e propria corsa tra investitori e colossi industriali. A contendersi il mercato è anche Harmonic, startup fondata dal CEO di Robinhood Vlad Tenev, che ha già raccolto 295 milioni di dollari. Harmonic ha lanciato Aristotle, un agente specializzato nel ragionamento matematico capace di verificare software scritto in linguaggio C e progetti di silicio in Verilog. La tecnologia è già in fase di sperimentazione presso giganti dei semiconduttori come Nvidia e Tensordyne.
Parallelamente, anche i laboratori di frontiera si stanno muovendo: Anthropic ha siglato una collaborazione strategica con la startup specializzata Theorem. Insieme hanno dimostrato come Claude sia stato in grado di individuare bug critici in librerie open source che trilioni di test tradizionali condotti nel corso degli anni non erano mai riusciti a intercettare, rilasciando contestualmente uno strumento integrato per consentire agli sviluppatori di avvalersi della verifica formale assistita direttamente nei loro flussi di lavoro.
Tra purezza teorica e realtà applicativa
Nonostante l'entusiasmo della Silicon Valley, parte della comunità ingegneristica invita alla prudenza. Figure come Will Wilson, alla guida della piattaforma di testing avanzato Antithesis, sottolineano come la verifica formale possa rivelarsi un'arma a doppio taglio: le prove matematiche sono infallibili solo finché reggono le assunzioni teoriche con cui sono state modellate. Nel mondo reale, guasti imprevisti dell'hardware, corruzioni fisiche della memoria o comportamenti anomali degli utenti sfuggono frequentemente alle premesse formali.
Inoltre, resta da comprendere quanto le aziende di software ordinario saranno disposte a pagare per una certificazione totale e quanto risulterà agevole integrare dimostratori di teoremi in pipeline di continuous delivery abituate a rilasci quotidiani.
Il punto di Mocchi's
Per chi come noi sviluppa software su misura e architetture enterprise, la verifica formale automatica non è una curiosità accademica ma l'evoluzione necessaria per governare l'ondata del codice assistito dall'IA. Generare codice a velocità vertiginosa senza strumenti di validazione matematica rischia di sommergere i team tecnici sotto una montagna di debito tecnico e vulnerabilità insidiose. Alle aziende italiane consigliamo di seguire questa transizione con pragmatismo: non occorrerà formalizzare ogni singola riga di interfaccia utente, ma iniziare ad applicare questi agenti di verifica ai moduli core, alla gestione dei pagamenti e alla sicurezza logica segnerà presto il confine tra software improvvisato e piattaforme di reale livello enterprise.