Degli agenti AI hanno riscritto il codice di CPython in Lean per trovare bug

Gli autori del progetto Formalizing CPython hanno utilizzato agenti AI autonomi per riscrivere il codice sorgente dell'interprete nel linguaggio di dimostrazione interattiva di teoremi Lean. Durante il lavoro, i sistemi hanno elaborato 613.318 righe della base di codice di CPython.

Nel processo di test automatizzato e di dimostrazione matematica della correttezza, gli agenti hanno identificato 418 bug. Tra le vulnerabilità e gli errori di programmazione rilevati, sono stati registrati 55 difetti che portano inevitabilmente all'arresto anomalo o al crash dell'interprete.

Il progetto dimostra l'applicabilità pratica dei metodi di verifica formale in combinazione con i modelli generativi per la ricerca di errori critici in software industriali su larga scala scritti in C.