Specula: generazione automatica di specifiche formali per la verifica del codice di sistema tramite IA

Specula è un sistema autonomo che genera specifiche formali di alta qualità per codice di sistema complesso con la semplice pressione di un pulsante, facilitando il model checking efficiente e la rilevazione di bug. Utilizza agenti di codifica basati su modelli linguistici di grandi dimensioni (LLM) per creare specifiche TLA+, che includono invarianti che definiscono proprietà di correttezza e modelli formali con astrazioni adeguate. Questo sistema completamente autonomo elimina la necessità di conoscenze umane nell'applicazione di metodi formali al codice pratico. Specula supera le sfide degli LLM come il reward hacking e le allucinazioni attraverso cicli di auto-miglioramento che aumentano la qualità delle specifiche approfondendo la comprensione del codice di sistema e dei comportamenti da parte degli agenti. Il sistema è stato valutato su 48 progetti open-source.