Non è un dettaglio accademico: la verifica formale del codice crittografico sta diventando un tassello operativo per chi distribuisce carichi sensibili in ambienti controllati. Microsoft ha appena pubblicato un ramo open source di SymCrypt, la libreria che protegge Windows e Azure, con prove matematiche che dimostrano la correttezza delle implementazioni Rust di SHA-3 e ML-KEM. Il lavoro, condotto con il proof assistant Lean e il traduttore Aeneas, segna un cambio di passo: dalla fiducia nei test alla certezza delle macchine.

Dallo standard NIST al modello verificabile

Il punto di partenza sono le specifiche pubbliche: per ML-KEM, ad esempio, la trasformata numerico-teorica (NTT) viene tradotta quasi riga per riga in Lean, mantenendo la struttura dei loop e gli aggiornamenti dei coefficienti. Questa prossimità sintattica non è un vezzo: rende il modello formale controllabile a occhio da revisori umani, che possono confrontare standard e specifica Lean fianco a fianco. In più, il modello è eseguibile, quindi lo si può testare contro i vettori ufficiali prima ancora di toccare il codice Rust.

Aeneas prende poi la funzione Rust scritta dagli ingegneri – mutuando array in-place, ottimizzazioni, gestione della memoria – e la trasforma in un modello puramente funzionale dentro Lean. La proprietà di borrow checking di Rust permette di eliminare a monte intere classi di ragionamento su aliasing e mutabilità, semplificando la prova. Il teorema finale dice: per ogni input che rispetta le precondizioni, l’implementazione restituisce lo stesso risultato del modello derivato dallo standard. Niente di meno.

Ottimizzazioni multi-architettura sotto tiro

La crittografia reale non può ignorare l’hardware. SymCrypt sfrutta intrinsics SSE2 su x86-64 e Neon su aarch64, con dispatch dinamico. Per verificare anche questi percorsi, il toolchain compila il codice Rust per ciascun target, produce modelli Lean separati e poi li unisce in un unico teorema che copre tutte le varianti. Dove servono wrapper a basso livello, si scrivono piccole specifiche Lean revisionate manualmente: la superficie trusted rimane minima, mentre le prestazioni restano intatte.

Questo è il punto che dovrebbe interessare chi gestisce server on-premise o air-gapped. Avere la certezza che gli algoritmi crittografici – inclusi quelli post-quantum già in distribuzione nelle build Insider di Windows – siano formalmente allineati allo standard NIST non è un lusso. Quando si esegue inference LLM in locale, i pesi del modello e i dati sensibili transitano su canali protetti proprio da quelle primitive. Una falla lì vanificherebbe qualsiasi architettura di sovranità.

Agenti al servizio della prova

Microsoft impiega agenti IA in due fasi: per abbozzare la traduzione degli standard in specifiche Lean (poi riviste) e per scrivere e riparare prove. Poiché Lean ha un kernel di verifica minimale, ogni script proposto da un agente viene comunque convalidato in modo deterministico. Il risultato è un’accelerazione notevole: lavoro che prima richiedeva mesi di specialista ora si può completare in tempi molto più brevi, con l’ingegnere che passa dal redigere ogni lemma a progettare la strategia di verifica e a revisionare i teoremi finali.

Le dashboard generate automaticamente espongono poi le garanzie in un linguaggio da developer: precondizioni, postcondizioni, funzioni coperte, assunzioni residue. Così chi scrive il codice Rust può verificare in autonomia se il teorema cattura davvero ciò che la funzione dovrebbe garantire, chiudendo il ciclo tra sviluppo e prova formale.

La combinazione di Rust, Lean, Aeneas e automazione agentica ridefinisce l’economia della verifica. Non si tratta più di un esercizio separato da laboratorio, ma di un processo integrato che accompagna il codice in produzione. Per i decisori IT che valutano stack on-premise, la presenza di crittografia verificata a valle di uno standard come NIST è un segnale strutturale: la fiducia non si delega più solo al vendor, ma si può (parzialmente) ispezionare. E in un’epoca in cui le minacce quantistiche iniziano a essere prese sul serio, non è un dettaglio.