L’ANALISI
Claude e verifica formale: che cosa provano davvero i 239 entry point
Anthropic e Theorem applicano Claude alla verifica formale di binari RISC-V: 239 entry point OSS-Fuzz nel progetto e 60 entry point pubblici riproducibili, con limiti espliciti su modello, input e proprietà.
In breve: Il risultato è sostanziale ma circoscritto: Claude ha generato prove Rocq che escludono crash rilevabili dalle proprietà modellate per 239 entry point OSS-Fuzz, su binari RISC-V e input fino a 64 MB. Il repository pubblico consente di ricontrollare 60 entry point in 25 librerie, ma non certifica che le librerie siano corrette, sicure in ogni ambiente o prive di vulnerabilità.
Che cosa è stato dimostrato
Anthropic descrive 239 entry point appartenenti a 123 librerie OSS-Fuzz. I target sono compilati in binari RISC-V e la specifica richiede che l’esecuzione termini senza crash, errori di memoria rilevati dai sanitizer o asserzioni fallite, per ogni input coperto fino a 64 MB e per le risposte del sistema operativo modellate.
Come funziona la catena di verifica
Theorem traduce istruzioni RISC-V e comportamento di processo Linux in LPS. Claude scrive la prova, mentre il kernel di Rocq controlla meccanicamente che la prova soddisfi il teorema. La fiducia non sparisce: si sposta sul modello RISC-V, sulla semantica Linux, sull’enunciato dimostrato e sul proof checker.
Scala del risultato e artefatti pubblici
Anthropic indica circa 180 milioni di righe di Rocq, con una prova tipica di circa 600.000 righe per binari con mediana di 18.000 istruzioni RISC-V. Il repository MIT pubblicato da Theorem contiene oggi prove per 60 entry point in 25 librerie, controllate con Rocq 9.2.0, oltre a istruzioni e inventario per riprodurre i controlli.
Perché non equivale a software sicuro
La prova riguarda i binari e le proprietà dichiarate, non ogni requisito funzionale. Un risultato errato, una perdita di memoria, codice morto, entry point non verificati, uso scorretto da parte del chiamante o difetti fuori dalla copertura dei sanitizer possono restare. Anche il modello LPS è esplicitamente incompleto e basato su assunzioni.
Che cosa cambia per chi sviluppa
Il punto pratico è la possibilità di trasformare fuzz target esistenti in specifiche formali e di far controllare le prove da un kernel indipendente dal modello. Prima di adottare il metodo su software critico servono però una proprietà utile, un confine di esecuzione realistico, artefatti riproducibili e revisione degli elementi fidati.
Condizioni e limitazioni
“Formalmente verificato” non significa software privo di bug. Le prove valgono per proprietà, binari, input e modello operativo specificati; LPS modella solo parte di Linux, ASan non rileva ogni difetto di memoria, non sono coperti tutti gli entry point né tutti gli usi delle librerie.
Checklist pratica
- Selezionare un singolo fuzz target con build riproducibile e commit fissato.
- Scrivere in linguaggio naturale la proprietà che si vuole realmente garantire.
- Controllare che input, memoria, threading, architettura e chiamate di sistema del modello rappresentino l’ambiente reale.
- Eseguire le prove pubbliche con la versione Rocq dichiarata prima di adattare la pipeline.
- Separare errori esclusi dai sanitizer da errori funzionali, leak e proprietà non modellate.
- Revisionare l’enunciato del teorema e le assunzioni LPS, non milioni di righe di prova generate.
- Mantenere fuzzing e test dinamici per superfici e configurazioni non coperte.
- Non usare il termine bug-free: documentare esattamente binario, proprietà e limiti verificati.