💻 computer science

Agentproof: Static Verification of Agent Workflow Graphs

Il paper presenta Agentproof, un sistema di verifica statica che estrae automaticamente modelli di grafo da quattro principali framework di agenti per rilevare difetti strutturali e violare politiche di sicurezza temporali prima della distribuzione, superando i limiti delle sole verifiche runtime.

Autori originali: Melwin Xavier, Vaisakh M A, Melveena Jolly, Midhun Xavier

Pubblicato 2026-03-24

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Melwin Xavier, Vaisakh M A, Melveena Jolly, Midhun Xavier

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di costruire un robot maggiordomo molto intelligente, capace di fare cose per te: inviare email, prenotare viaggi, gestire i tuoi conti bancari. Per dargli istruzioni, non gli scrivi un lungo manuale; gli disegni una mappa (un grafico) che mostra passo dopo passo cosa deve fare.

"Se l'email è urgente, vai al passo A."
"Se è normale, vai al passo B."
"Alla fine, manda la mail."

Il problema è che, quando disegni questa mappa, potresti fare un errore di penna: potresti dimenticare di collegare il passo "Scrivi bozza" al passo "Invia email". Il robot, quando arriverà a quel punto, si fermerà per sempre, bloccato in un vicolo cieco, senza che tu te ne accorga finché non provi a usarlo.

Oggi, i sistemi di sicurezza controllano il robot mentre lavora (come un guardiano che ti ferma se dici una parolaccia). Ma questo non ti dice se la tua mappa è sbagliata. Se il robot non prova mai quel percorso sbagliato, il guardiano non lo vede mai.

Agentproof è come un ispettore di sicurezza che arriva prima che il robot venga messo in servizio.

Ecco come funziona, spiegato con analogie semplici:

1. Il Traduttore Universale (L'Estrattore)

Esistono diversi modi per disegnare queste mappe robotiche (come se usassi Google Maps, Waze o una mappa cartacea). Ogni "linguaggio" è diverso.

Agentproof ha un "traduttore magico" che legge le istruzioni scritte in questi 4 linguaggi diversi (LangGraph, CrewAI, AutoGen, Google ADK) e le trasforma tutte in una singola mappa standard che il computer può capire perfettamente. Non devi riscrivere nulla a mano.

2. L'Ispettore che controlla la Mappa (Verifica Strutturale)

Una volta ottenuta la mappa standard, Agentproof la esamina con una lente d'ingrandimento per cercare errori logici, senza far muovere il robot:

Il Vicolo Cieco: "Ehi, qui c'è un passaggio che non porta da nessuna parte! Se il robot ci finisce, si blocca."
La Porta Bloccata: "C'è un'uscita che non si può raggiungere da nessuna parte. Il robot non potrà mai finire il lavoro."
Il Controllo Umano Mancante: "Stai per chiedere al robot di cancellare un conto bancario, ma non hai messo un passaggio dove un umano deve dire 'Sì, procedi'. È pericoloso!"

Se trova un errore, non ti dice solo "C'è un errore". Ti dà un biglietto di prova (una "witness trace"): ti mostra esattamente il percorso che il robot farebbe per finire bloccato, così puoi correggerlo subito.

3. Le Regole del Gioco (Politiche Temporali)

Oltre a controllare la mappa, Agentproof può leggere le regole che vuoi imporre al robot. Immagina di dire:

"Prima di inviare una mail, devi sempre averla letta un umano."
"Non puoi mai cancellare un database."

Agentproof trasforma queste regole in piccoli robot controllori (automi) che corrono sulla tua mappa. Controllano se, seguendo qualsiasi strada possibile, il robot potrebbe mai violare queste regole. Se la mappa permette una strada dove il robot salta il controllo umano, Agentproof ti avvisa prima che il robot venga mai usato.

Perché è importante?

Fino a oggi, per essere sicuri che un robot fosse sicuro, dovevi:

Scrivere tutto a mano in un linguaggio complicato (come tradurre un libro in un codice segreto).
Farlo girare milioni di volte per vedere se si rompeva (e sperare di trovare l'errore).

Agentproof fa tutto da solo, in meno di un secondo, anche per mappe enormi.

Non serve riscrivere nulla: Legge direttamente il codice che hai già scritto.
Non serve aspettare: Trova gli errori mentre li disegni, non dopo che il robot ha fatto danni.
È un doppio livello di sicurezza: I controlli "in tempo reale" (il guardiano) servono ancora per fermare le parole cattive o gli errori del robot mentre parla, ma Agentproof si assicura che la struttura del lavoro sia solida e sicura.

In sintesi: Agentproof è l'architetto che controlla i progetti di un edificio prima che venga costruito, assicurandosi che non ci siano scale che portano al nulla o porte che non si aprono, così che quando il robot (l'edificio) viene aperto, funzioni perfettamente.

1. Il Problema

Con l'adozione crescente di framework per agenti basati su LLM (come LangGraph, CrewAI, AutoGen e Google ADK), il comportamento degli agenti viene sempre più codificato come grafi di workflow espliciti. Tuttavia, l'attuazione delle misure di sicurezza rimane prevalentemente un problema a runtime.

Gli strumenti di sicurezza attuali (es. NeMo Guardrails, LlamaGuard) operano intervenendo sulle singole chiamate LLM o sugli inviti ai tool, applicando filtri basati sul contenuto. Questo approccio presenta tre limitazioni fondamentali:

Overhead di latenza: Ogni chiamata subisce un ritardo.
Copertura reattiva: Rilevano le violazioni solo se il percorso di esecuzione offensivo viene effettivamente esercitato.
Mancanza di garanzie di copertura: Non possono garantire la sicurezza di percorsi che non vengono testati.

Inoltre, esistono difetti topologici (strutturali) nel grafo del workflow che gli strumenti di runtime non possono rilevare, a meno che il percorso difettoso non venga attivato. Un esempio classico è un "nodo morto" (dead-end) o un'uscita irraggiungibile causata da un errore di sviluppo: un agente potrebbe bloccarsi silenziosamente su un percorso specifico senza che un guardrail runtime se ne accorga mai.

2. Metodologia: Agentproof

Il paper presenta Agentproof, un sistema per la verifica statica pre-deploy dei workflow degli agenti. L'approccio si basa sull'osservazione che i moderni framework espongono la struttura del workflow tramite le loro API, rendendola estraibile e analizzabile automaticamente.

Il sistema opera attraverso una pipeline in cinque fasi:

Estrazione del Grafo (Cross-Framework):
- Agentproof include estrattori specifici per quattro framework principali: LangGraph, CrewAI, AutoGen e Google ADK.
- Questi estrattori mappano le rappresentazioni eterogenee di ciascun framework in un modello di grafo astratto unificato (AgentGraph).
- Il modello unificato definisce nodi tipizzati (entry, exit, tool, LLM, router, human, subgraph) e archi tipizzati (diretti, condizionali, paralleli, loop).
- Questo elimina la necessità di modellazione manuale richiesta dai model checker generici.
Verifica Strutturale:
- Vengono eseguiti sei controlli strutturali sul grafo estratto utilizzando algoritmi di visita standard (BFS/DFS) con complessità lineare $O(|V| + |E|)$ .
- I controlli includono:
  - Raggiungibilità delle uscite: Verifica che ogni nodo raggiungibile possa portare a un'uscita.
  - Rilevamento Dead-end: Identifica nodi senza archi in uscita (esclusi gli exit).
  - Verifica della forma dei Router: Assicura che gli archi uscenti dai router siano etichettati come condizionali.
  - Presenza di Gate Umani: Verifica l'esistenza di nodi di approvazione umana o la copertura di percorsi verso tool sensibili.
  - Dichiarazione dei Tool: Assicura che i nodi tool abbiano nomi di tool dichiarati.
- In caso di fallimento, il sistema genera una traccia testimone (witness trace) che mostra il percorso esatto del difetto.
Verifica Temporale (Statica e Runtime):
- Viene definito un DSL (Domain Specific Language) per le policy di sicurezza, che copre il frammento di sicurezza della LTL (Linear Temporal Logic).
- Le policy vengono compilate in Automati Finiti Deterministici (DFA).
- Verifica Statica: Viene eseguita una costruzione del prodotto tra il grafo del workflow e il DFA. Questo permette di esplorare tutti i percorsi possibili del grafo senza eseguirli, rilevando violazioni temporali (es. "un tool distruttivo non deve mai essere chiamato dopo un draft email").
- Monitoraggio Runtime: I DFA possono anche essere eseguiti su flussi di eventi reali o simulati.

3. Contributi Chiave

Pipeline di Estrazione Cross-Framework: La prima soluzione in grado di estrarre automaticamente modelli di workflow da quattro framework diversi, normalizzandoli in un'unica rappresentazione analizzabile senza intervento umano.
Pipeline di Verifica Pre-Deploy: Un sistema completo che combina controlli strutturali (per difetti topologici) e policy temporali (per vincoli di sequenza), supportando sia la verifica statica esaustiva che il monitoraggio runtime.
Valutazione Empirica: Un benchmark curato di 18 workflow che dimostra l'efficacia del sistema nel rilevare difetti strutturali e violazioni di policy, con tempi di verifica inferiori al secondo anche per grafi di grandi dimensioni.
Distinzione tra Difetti Strutturali e Violazioni di Policy: Il lavoro chiarisce la differenza tra errori topologici (es. nodi morti) e violazioni di policy (es. mancanza di gate umani), categorie che la ricerca precedente tendeva a confondere.

4. Risultati

L'approccio è stato valutato su un corpus di 18 workflow costruiti dagli autori, rappresentativi di pattern comuni e anti-pattern:

Rilevamento Difetti:
- Il 27% dei workflow nel benchmark conteneva difetti strutturali (nodi morti, uscite irraggiungibili, loop senza uscita).
- Il 55% violava una policy di "gate umano" quando questa era richiesta.
- Agentproof ha rilevato con successo tutti i difetti strutturali e le violazioni di policy.
Prestazioni:
- La verifica strutturale è estremamente veloce: per grafi fino a 5.000 nodi, il tempo di verifica è inferiore a 105 ms (sub-secondo).
- La compilazione e valutazione dei monitor temporali sono indipendenti dalla dimensione del grafo.
DSL: Tutti i 15 policy di sicurezza temporali definiti (basati su requisiti reali come GDPR, SOC 2, OWASP) rientravano nel frammento di 7 forme del DSL, confermando che la complessità espressa è sufficiente per le esigenze pratiche di sicurezza.
Precisione: I controlli strutturali hanno raggiunto una precisione perfetta (P=1.0), mentre il controllo sulla presenza umana ha mostrato un falso positivo (P=0.75) in un caso a basso rischio dove la supervisione umana era discutibile.

5. Significato e Implicazioni

Il lavoro di Agentproof rappresenta un passo significativo verso la sicurezza degli agenti AI:

Complementarità: Non sostituisce i guardrail runtime, ma li completa. La verifica statica cattura difetti topologici che il runtime non può vedere a meno che non vengano attivati, riducendo la superficie di attacco che i controlli runtime devono gestire.
Automazione: Elimina l'ostacolo della modellazione manuale, rendendo la verifica formale accessibile agli sviluppatori di agenti che non sono esperti di metodi formali.
Scalabilità: Dimostra che l'analisi statica dei workflow degli agenti è fattibile e scalabile, anche man mano che i sistemi diventano più complessi (multi-agente, gerarchici).
Sicurezza Proattiva: Sposta il rilevamento dei difetti dalla fase di esecuzione (dove possono causare danni) alla fase di sviluppo/deploy, permettendo di correggere errori di progettazione prima che l'agente venga messo in produzione.

In sintesi, Agentproof fornisce un framework pratico per garantire la correttezza strutturale dei workflow degli agenti, colmando il divario tra la modellazione grafica esposta dalle API dei framework e le tecniche di verifica formale.