IA e verifica formale: cosa dimostrano davvero le nuove prove

Quando un assistente completa una funzione in pochi secondi, il codice può sembrare convincente e tuttavia fallire proprio nei casi meno comuni. I test tradizionali provano una selezione di input; la verifica formale affronta una domanda diversa: date proprietà esplicite e un modello preciso del programma, si può dimostrare che il comportamento le rispetta in tutti i casi coperti? L’intelligenza artificiale sta rendendo più accessibile la costruzione di queste dimostrazioni, ma non trasforma automaticamente ogni risultato in una garanzia generale di sicurezza.

Due sviluppi recenti mostrano bene sia il potenziale sia le differenze tra gli approcci. Un lavoro di ricercatori di Stanford presenta CryptoProver, un sistema per costruire specifiche e prove per librerie crittografiche Rust; Anthropic e Theorem descrivono invece prove su binari compilati di numerosi progetti open source. Harmonic, infine, ha esteso il proprio agente Aristotle alla verifica di software C e circuiti Verilog. Non sono tre versioni dello stesso prodotto: cambiano il codice esaminato, le proprietà dimostrate e le ipotesi necessarie.

Che cosa significa “dimostrare” un programma

Una prova formale collega un’implementazione a una specifica: una descrizione matematica di ciò che il software dovrebbe fare. Se la specifica è incompleta o sbagliata, il sistema può dimostrare correttamente una proprietà che non corrisponde all’aspettativa dell’utente. Anche il perimetro conta: una prova può riguardare una funzione, un percorso d’ingresso o una classe di errori, non necessariamente ogni comportamento dell’applicazione completa.

Questo distingue la verifica dai test senza renderli avversari. Un test esegue concretamente il programma con alcuni dati; il fuzzing genera moltissimi input per cercare crash o risultati anomali. Una dimostrazione, invece, può coprire tutti gli input entro un modello e una specifica determinati. La copertura universale non è illimitata: dipende da ciò che è stato formalizzato, dagli strumenti fidati e dalle condizioni dichiarate.

Tre esperimenti, tre perimetri diversi

CryptoProver affronta il costo di descrivere e provare proprietà di codice crittografico già esistente. Il paper presenta una verifica indipendente della libreria curve25519-dalek e del codice chacha20 di RustCrypto, usando Verus e un’architettura “trust-first” che impone controlli meccanici ai risultati prodotti dal modello. Il contributo interessante non è una certificazione indistinta di Signal o di tutte le applicazioni che usano queste librerie: è un metodo per ricostruire specifiche interne e collegarle a implementazioni reali. Le dipendenze e le proprietà dimostrate vanno quindi lette nel dettaglio del lavoro, non dedotte dal nome di un’app che utilizza la crittografia.

Anthropic e Theorem hanno pubblicato un esperimento più ampio su programmi open source: Claude ha prodotto prove verificate dal kernel Rocq per proprietà di non-crash associate a fuzz test di 239 punti d’ingresso in 123 librerie OSS-Fuzz. Il modello opera sui binari RISC-V e sul modello formale del sistema descritto dagli autori. Questo consente di escludere crash entro quel perimetro, ma non equivale a dimostrare che l’intera libreria sia priva di bug. Le prove non coprono ogni funzione, ogni architettura o ogni condizione di esecuzione; inoltre una specifica di test non dimostra da sola che il comportamento sia quello desiderato in ogni contesto reale.

Harmonic dichiara che Aristotle può lavorare con C e Verilog, proporre proprietà a partire dal codice e indicare quali sono state provate e con quali assunzioni. L’azienda presenta esempi su Tensordyne e LibTomMath e offre il servizio con tariffazione basata sul consumo. Sono risultati e caratteristiche comunicati dal fornitore: per valutarli in un progetto concreto servono la specifica adottata, l’ispezione delle prove e la possibilità di riprodurre i controlli nel proprio flusso di sviluppo.

Come valutare uno strumento senza scambiare la prova per una promessa

Per un team software, la prima domanda non è quale modello abbia ottenuto il risultato più spettacolare, ma quale proprietà serve dimostrare. Si vuole evitare un accesso fuori dai limiti, garantire che una funzione rispetti un protocollo o verificare la correttezza di una trasformazione? Senza una risposta precisa, l’automazione può produrre una dimostrazione formalmente valida ma poco utile.

Conviene poi chiedere quale parte del sistema entra nella prova: sorgente o binario, singola routine o progetto più ampio, quali compilatore, librerie e modelli hardware/software sono assunti corretti. È importante capire anche chi controlla il risultato. Un proof checker indipendente può verificare la validità logica della dimostrazione, ma non decide se la specifica sia adeguata né se il modello del processore e del sistema operativo rappresenti tutte le condizioni d’uso.

Infine, la prova va integrata nella manutenzione: versione del codice, specifica, dipendenze e controlli automatici devono restare allineati. Una modifica successiva può invalidare il risultato o richiedere una nuova dimostrazione. Test, revisione del codice, analisi statica e verifica formale possono quindi completarsi a vicenda. L’IA riduce parte del lavoro specialistico necessario per formulare invarianti e costruire prove; non elimina la responsabilità di scegliere ciò che conta e verificare che il risultato sia applicabile.

Per chi sviluppa software, la novità concreta è che alcune attività prima riservate a gruppi specializzati possono essere tentate su porzioni più ampie di codice e con costi inferiori. Il passo prudente è partire da una proprietà circoscritta e critica, misurare quanto lavoro umano resta e controllare le ipotesi. “Formalmente verificato” ha valore quando si sa esattamente quale affermazione è stata provata, per quale versione e sotto quali condizioni.