Sintesi Tecnica: Programmazione "Vibe" Guidata da Metodi Formali tramite Ingegneria Orientata ai Modelli

1. Definizione del Problema

Il documento affronta il divario critico tra la rapida adozione della "vibe coding" — un flusso di lavoro in cui gli sviluppatori descrivono l'intento in linguaggio naturale a modelli linguistici di grandi dimensioni (LLM) e accettano il codice generato con una revisione minima — e i rigorosi requisiti di garanzia per i sistemi critici per la sicurezza (regolati da standard come DO-178C, IEC 61508 e ISO 26262).

Gli approcci attuali per verificare il codice generato da LLM affrontano due barriere strutturali primarie:

1. Linguaggi orientati alla verifica: I metodi rivolti a linguaggi come Dafny, Verus o Lean soffrono di scarsità di dati di pre-addestramento per gli LLM, scarse capacità di ragionamento compositivo e una mancanza di integrazione con le esistenti catene di strumenti industriali (che utilizzano prevalentemente Java, C o C++).
2. Filtraggio Post-Hoc: Gli strumenti esistenti che aggiungono strati di verifica dopo la generazione trattano la verifica come un filtro piuttosto che come un segnale di feedback, non offrendo alcun meccanismo per guidare l'LLM verso la correttezza.

Di conseguenza, la "vibe coding" non guidata produce artefatti che mancano delle garanzie di correttezza formale e delle prove tracciabili richieste per la certificazione.

2. Metodologia: La Pipeline Forge

Gli autori presentano Forge (Formal method Oriented Refinement loop for GEnerated code), una pipeline a ciclo chiuso che integra la generazione tramite LLM con un'infrastruttura consolidata di Ingegneria Orientata ai Modelli (MDE). La filosofia centrale è trattare l'LLM come un "generatore di bozze" e la catena MDE come un "discriminatore", permettendo agli sviluppatori di lavorare in Java mainstream mentre la verifica formale opera su modelli estratti che non devono mai vedere.

La pipeline consiste in sette fasi raggruppate in tre famiglie:

Fase 1: Elicitazione dei Requisiti

I requisiti in linguaggio naturale vengono strutturati in un insieme di requisiti formali.

Fase 2: Sintesi del Codice Top-Down (Vibe Coding)

Un LLM (specificamente Anthropic Claude Code) genera codice sorgente Java basandosi su una sequenza di cinque livelli di prompt:

1. Architettura: Struttura di pacchetti/classi e mappatura dai requisiti alle classi.
2. Skeleton (Scheletro): Java compilabile con metodi stubbed.
3. Leaves (Foglie): Logica di sensori, attuatori e operazioni.
4. Controller: La logica della macchina a stati annidata per modalità.
5. Review (Revisione): Auto-segnalazione di default inventati.

Vincoli: Per garantire un'estrazione del modello fedele, l'LLM è limitato a un sottoinsieme specifico di Java (ad esempio, niente lambda, stream o pattern matching; le macchine a stati devono usare strutture if-else a due livelli). Questo sottoinsieme è motivato dalla trattabilità dell'estrazione del modello piuttosto che dalla prevedibilità del runtime.

Controlli Pre-volo (2a–2c): Il codice generato viene sottoposto a compilazione, controlli di copertura requisito-codice e linting strutturale rispetto alle regole di estrazione.

Fasi 3–5: Estrazione e Trasformazione

Questa fase converte il codice Java in artefatti formali senza intervento umano:

• Fase 3 (Text-to-Model): Un ponte personalizzato Spoon-to-EMF analizza l'AST Java (supportando funzionalità Java 17+ come interfacce sigillate e record) in un modello Eclipse Modeling Framework (EMF).
• Fase 4 (Model-to-Model): Uno script Epsilon Transformation Language (ETL) trasforma il modello Java EMF in una macchina a stati RoboChart, identificando modalità, transizioni e guardie.
• Fase 5 (Model-to-Text): Tre artefatti formali indipendenti vengono generati:
  1. Specifiche Dafny: Generate direttamente dal modello Java EMF per la verifica deduttiva.
  2. Script CSP-M: Generati dal modello RoboChart per la verifica del raffinamento comportamentale.
  3. Teorie Isabelle/HOL: Generate dal modello RoboChart utilizzando la notazione Z-Machine per la dimostrazione dei teoremi.

Fasi 6–7: Verifica e Raffinamento a Ciclo Chiuso

• Fase 6 (Verifica): I tre artefatti sono verificati dai rispettivi strumenti:
  • Dafny (Z3): Controlla i contratti a livello di funzione (precondizioni/postcondizioni, terminazione).
  • FDR4: Controlla le proprietà comportamentali (assenza di deadlock, assenza di divergenza) tramite il raffinamento CSP.
  • Isabelle/HOL: Dimostra gli invarianti strutturali e l'assenza di deadlock sulla relazione di transizione simbolica.
  • Audit di Vacuità (6d): Assicura che le prove non siano banali (ad esempio, non solo true o True).
• Fase 7 (Raffinamento): I fallimenti della verifica vengono tradotti in prompt di correzione strutturati e azionabili (JSON/Markdown). Questi prompt, collegati a specifici requisiti e righe di codice tramite una catena di tracciabilità, vengono forniti all'LLM per rigenerare il codice. Il ciclo continua finché tutti i verificatori passano o viene raggiunto un numero massimo di iterazioni.

3. Contributi Chiave

1. Ciclo Closed Draft-and-Discriminate: Un'archiaettura innovativa in cui il codice mainstream generato da LLM viene reso formalmente verificabile attraverso il routing verso l'infrastruttura MDE, utilizzando i fallimenti di verifica come segnali di correzione iterativi invece di filtri post-hoc.
2. Ponte Spoon-to-EMF: La prima trasformazione text-to-model nativa di EMF per il moderno Java (17+), capace di gestire interfacce sigillate, record e sintassi di pattern, colmando una lacuna lasciata da strumenti legacy come MoDisco.
3. Design a Tre Verificatori Complementari: Un sistema che impiega Dafny, FDR4 e Isabelle/HOL in parallelo. Il documento dimostra che questi verificatori non sono intercambiabili; ognuno cattura classi distinte di difetti (ad esempio, Dafny cattura violazioni di contratto, FDR4 cattura deadlock comportamentali, Isabelle cattura deadlock strutturali).
4. Tracciabilità End-to-End: Una catena completamente tracciabile che collega i requisiti in linguaggio naturale attraverso il codice sorgente generato, i modelli intermedi e le prove formali, consentendo direttive di correzione per singolo requisito.
5. Validazione Empirica: Evidenza che il ciclo converge verso codice completamente verificato attraverso molteplici esecuzioni indipendenti, guidato specificamente dal feedback del verificatore.

4. Risultati Sperimentali

La pipeline è stata valutata su tre casi di studio scritti esternamente di complessità crescente:

• SRanger: Un robot terrestre a singolo controller (23 requisiti, ~220 LOC).
• Last Response Engine (LRE): Un governatore di sicurezza per AUV (51 requisiti, ~613 LOC).
• Chemical Detector: Un robot autonomo multi-controller (81 requisiti, ~618 LOC).

Risultati Chiave:

• Convergenza: In 15 esecuzioni indipendenti (5 per ogni caso di studio), tutte le 15 esecuzioni sono confluite verso codice completamente verificato entro 2 o 3 iterazioni (mediana 2).
• Necessità di Feedback: In un esperimento "cold-baseline" (30 esecuzioni senza feedback del verificatore), 0 esecuzioni sono confluite. La generazione a passaggio singolo ha fallito nel produrre codice verificato.
• Ruolo dei Verificatori: Un'ablazione "compile-only" (dove il feedback del verificatore era nascosto ma i controlli di compilazione rimanevano) ha mostrato che tutte le 15 esecuzioni hanno comunque prodotto artefatti che fallivano almeno un verificatore formale. Ciò conferma che il feedback del verificatore, e non solo l'iterazione o la compilazione, guida la convergenza.
• Rilevamento Difetti: I tre verificatori hanno catturato difetti distinti. Ad esempio, un deadlock strutturale in una modalità terminale è stato mancato da Dafny e FDR4 ma catturato da Isabelle, richiedendo una correzione specifica (aggiunta di un auto-loop di idle).
• Costo: La convergenza ha richiesto tipicamente 2-3 iterazioni. Il tempo di esecuzione (wall-clock time) è variato da circa 1 a 15 minuti per esecuzione, dominato dai tempi di prova di Isabelle in presenza di problemi strutturali.

5. Significato e Rivendicazioni

Il documento sostiene di dimostrare un argomento strutturale su dove risieda la verifica formale in un workflow guidato da LLM: non dentro l'LLM, e non come filtro post-hoc, ma come discriminatore in un processo di raffinamento a ciclo chiuso.

• Rilevanza per la Certificazione: La pipeline produce tipi di evidenza riconosciuti dagli standard di sicurezza (verifica deduttiva, controllo del raffinamento e dimostrazione dei teoremi), offrendo una via verso la certificazione del codice generato da IA senza richiedere agli ingegneri di imparare linguaggi formali o abbandonare le esistenti catene di strumenti Java.
• Fattibilità: Dimostra che il codice generato da LLM in linguaggi mainstream può essere sistematicamente trasformato in modelli formali e verificato, a patto che sia presente una robusta pipeline di estrazione e trasformazione.
• Modestia: Gli autori dichiarano esplicitamente che questo lavoro fornisce evidenze verso un caso di certificazione, non la certificazione stessa. Riconoscono che la certificazione completa richiederebbe ulteriori passaggi, tra cui la qualifica degli strumenti, le evidenze di processo e la revisione indipendente del caso di assurance, che rimangono lavori futuri. Il contributo è l'esistenza di una pipeline vitale che chiude il ciclo di verifica.