Nel mantenere alcuni progetti OSS, mi è capitato di voler provare i famosi “agenti AI”, quelli che non si limitano a rispondere alle domande ma fanno cose. E così ho potuto farmi un’idea anche sulla questione se questi agenti possano davvero “programmare”, cioè sostituire un programmatore, magari junior.

La risposta alla quale sono arrivato è, sostanzialmente: no.

Ma possono fare qualcosa che sta a metà strada fra “sostituire un programmatore” e “non servire a nulla”: possono scrivere il codice che avete già ideato.

---

L’esempio nasce dal fatto che ho deciso di riprendere un linguaggio bellissimo, Ada, che avevo usato parecchi anni fa nel mondo ferroviario italiano, tanto per rinfrescarmi la memoria.

E nel frattempo c’è SPARK.

SPARK è un sottoinsieme ed estensione di Ada pensato espressamente per software ad alta affidabilità e verifica formale. In altre parole, oltre a compilare il programma potete descrivere, direttamente nel linguaggio, proprietà che quel programma deve rispettare e poi chiedere alla toolchain di dimostrare matematicamente che le rispetti.

Non sto parlando di commenti nei quali scrivete che secondo voi la funzione dovrebbe fare una certa cosa. Sto parlando di precondizioni, postcondizioni, invarianti e contratti che fanno parte della descrizione formale del programma e che strumenti come GNATprove cercano effettivamente di dimostrare.

In termini molto brutali: scrivete del codice e dite che, se entra una certa classe di valori, deve uscire qualcosa con determinate proprietà. Il sistema trasforma il problema in formule logiche e cerca di provarle. Se ci riesce, avete una dimostrazione rispetto alle proprietà che avete specificato. Se non ci riesce, non avete quella dimostrazione.

Ovviamente il concetto di verifica formale ha qualche dettaglio da approfondire.

Supponiamo che il vostro programma faccia una chiamata a Internet. Come fate a “dimostrare matematicamente Internet”, intesa come teorema?

Non potete.

Non potete dimostrare che quel server domani esisterà. Non potete dimostrare che risponderà. Non potete dimostrare che non cadrà la rete. E non potete dimostrare matematicamente che dall’altra parte qualcuno non abbia cambiato completamente il comportamento del servizio.

Potete però delimitare il problema.

Per esempio, potete mettere davanti alla risposta della rete un wrapper e specificare qualcosa del tipo: qualsiasi sequenza di dati mi arrivi da fuori, questa funzione restituirà o un JSON che soddisfa una certa struttura oppure un risultato vuoto e ben definito. Nessun buffer overflow, nessun valore fuori range, nessuno stato del programma che non avevate previsto.

Questo sì che potete provare.

Ed è importante capire cosa significhi, perché altrimenti arriva immediatamente qualcuno a dire: “Ah, quindi sostieni che esista il codice perfetto”.

No.

Dimostrare formalmente che un programma soddisfa una specifica non significa affatto dimostrare che la specifica sia intelligente.

Potete dimostrare matematicamente che il programma farà esattamente quello che gli avete ordinato di fare, per tutti gli stati coperti dal modello. Rimane però una domanda piuttosto importante:

gli avete ordinato di fare la cosa giusta?

La storia dell’Ariane 5 è un esempio famoso, anche se viene spesso raccontata male.

Il 4 giugno 1996, il primo Ariane 5 andò distrutto circa quaranta secondi dopo l’inizio della sequenza di volo. Il problema partì dal software del sistema di riferimento inerziale, largamente riutilizzato dall’Ariane 4. Un valore relativo alla velocità orizzontale, perfettamente possibile nella traiettoria molto più aggressiva dell’Ariane 5, venne convertito da un numero floating point a 64 bit in un intero con segno a 16 bit. Il valore non ci stava. Si verificò un overflow.

La cosa particolarmente istruttiva è che fallirono praticamente insieme sia il sistema inerziale principale sia quello di riserva, perché eseguivano lo stesso software e incontrarono la stessa condizione. I dati diagnostici prodotti dal sistema guasto finirono poi interpretati dal computer di bordo come dati di volo, provocando comandi assurdi agli attuatori. Il razzo deviò violentemente, si disintegrò e il sistema di autodistruzione intervenne correttamente quando si ruppero i collegamenti fra i booster e lo stadio centrale.

Quel pezzo di software proveniva da un sistema nel quale certe grandezze erano state implicitamente considerate abbastanza piccole da poter essere rappresentate in quel formato. Sull’Ariane 4 quell’assunzione aveva senso. Sull’Ariane 5 non più.

Il programma non aveva improvvisamente sviluppato cattive intenzioni. Era l’assunzione sulla quale era costruito a non corrispondere più al mondo nel quale lo avevano messo.

Quindi chiariamo bene cosa significa verifica formale.

Significa che potete dimostrare matematicamente determinate proprietà del programma rispetto a un modello, a dei contratti e a delle assunzioni.

Non significa che il modello rappresenti correttamente il mondo.

Non significa che le assunzioni siano vere.

E soprattutto non significa che quello che avete chiesto al programma di fare sia una buona idea.

---

Ma il punto è che il programma fece esattamente quello che doveva, perché era progettato per comportarsi in maniera deterministica anche in presenza di errori gravi. Il problema, come abbiamo visto, era che una delle assunzioni sul mondo esterno era sbagliata.

Detto questo, ci siamo.

Nel programmare Xenomorph ho deciso di usare uno spool sul modello di quello dei server SMTP. Per rappresentarlo ho usato un automa a stati finiti deterministico.

Ed è una cosa estremamente comoda, perché a quel punto posso descrivere matematicamente il comportamento dello spool e poi chiedere alla toolchain di verificare che l'implementazione rispetti proprio quella struttura.

Formalmente, un automa a stati finiti deterministico si definisce così:

M = (Q, Sigma, delta, q0, F)

dove:

Q
    e' un insieme finito e non vuoto di stati.

Sigma
    e' un alfabeto finito di input, oppure, nel mio caso,
    l'insieme finito degli eventi che possono interessare lo spool.

delta
    e' la funzione di transizione:

        delta : Q x Sigma -> Q

Essendo una funzione, per ogni stato q in Q
e per ogni input a in Sigma esiste uno e un solo
stato successivo q' tale che:

        delta(q, a) = q'

q0
    e' lo stato iniziale:

        q0 in Q

F
    e' l'insieme degli stati finali o terminali:

        F subseteq Q


Per dimostrare anche che il sistema non possa rimanere
intrappolato per sempre in un ciclo, si puo' introdurre
una funzione di rango:

    rank : Q -> N

dove N e' l'insieme dei numeri naturali.

Si richiede poi che per ogni transizione non terminale:

    delta(q, a) = q'  =>  rank(q') < rank(q)

In altre parole, ogni transizione utile deve portare
a uno stato con rango strettamente minore.

Poiche' nei numeri naturali non puo' esistere una
sequenza strettamente decrescente infinita, non puo'
esistere nemmeno un'esecuzione infinita composta
esclusivamente da tali transizioni.

Quindi, se ogni stato raggiungibile non terminale
possiede una transizione che riduce il rango,
il sistema deve prima o poi raggiungere uno stato
terminale appartenente a F.

Nel mio caso, gli elementi di Q non sono concetti particolarmente esoterici: sono cose come “messaggio ricevuto”, “validato”, “in coda”, “in consegna”, “consegnato”, “fallito”.

Gli elementi di Sigma, invece, sono eventi: validazione riuscita, validazione fallita, consegna riuscita, errore di consegna, timeout, retry, e così via.

La cosa importante è che la proprietà “deterministico” da sola non basta a dimostrare che un messaggio arriverà necessariamente alla fine.

Un automa deterministico può benissimo avere un ciclo:

A -> B
B -> A

e restarci per sempre.

Quello che serve in più è una proprietà di progresso.

Ed è qui che entra in gioco il rango: se riesco ad associare a ogni stato un numero naturale e dimostrare che, a ogni avanzamento reale dello spool, quel numero diminuisce, allora ho qualcosa di molto più forte del semplice “ho scritto una macchina a stati”.

Ho una dimostrazione che il messaggio non può continuare a vagare indefinitamente.

Prima o poi deve finire in uno stato terminale.

E soprattutto deve finirci seguendo precisamente le transizioni che ho deciso io.

---

Voi direte: ma cazzo, per scrivere del codice devi anche tenere conto della sua descrizione matematica e della teoria dei linguaggi formali? Il tuo papero di gomma si chiama Noam Chomsky?

Sì.

E prima o poi mi farò degli sticker con scritto:

“Il mio papero di gomma si chiama Noam Chomsky.”

Oppure:

“Niklaus Wirth mi spiccia casa.”

E soltanto il due per mille delle persone che li vedranno capirà perché fanno ridere. Ma sarà il due per mille giusto.

Seriamente: diciamo pure che Ada/SPARK è roba di nicchia. La trovate soprattutto in quei mondi nei quali un errore software può costare parecchio: aerospazio, ferroviario, difesa, sistemi industriali ad alta affidabilità e, in generale, tutti quei posti dove una certa dose di paranoia fa bene alla salute.

Ma lo sapete: a me non piace vincere facile.

---

E qui finalmente arriviamo al punto.

Se usiamo un agente AI come aiuto alla programmazione, scopriamo una cosa interessante.

Gli diamo una specifica abbastanza precisa e, inizialmente, lui la segue. Continuiamo però a lavorare: gli chiediamo nuove funzioni, correzioni, refactoring, modifiche. Il contesto cresce, cresce il codice e soprattutto cresce il numero dei vincoli che dovrebbe continuare a ricordare contemporaneamente.

A un certo punto può cominciare a violarne qualcuno.

Non necessariamente perché sia “diventato stupido”, e nemmeno esclusivamente perché il modello sia stocastico. Il problema più generale è che gli LLM attuali non mantengono perfettamente i vincoli quando le istruzioni diventano lunghe, numerose e distribuite lungo conversazioni complesse. Ed è esattamente il genere di problema che si incontra usando un agente per modificare una codebase per parecchio tempo.

Nel mio caso me ne sono accorto perché GNATprove ha cominciato a protestare.

Non dicendo, ovviamente, “Ehi, Uriel, questo non è più un automa a stati”. Il prover non conosce le mie intenzioni metafisiche.

Semplicemente, non riusciva più a dimostrare alcune delle proprietà e degli invarianti con i quali avevo descritto formalmente lo spool.

Perché?

L'agente aveva deciso di ottimizzare.

E quando un software contemporaneo decide di ottimizzare, spesso prima o poi arriva la risposta rituale:

“Mettiamoci una cache.”

Aveva quindi introdotto una cache in RAM per evitare di andare continuamente a rileggere lo stato dello spool dal filesystem.

Dal punto di vista prestazionale l'idea aveva perfettamente senso.

Dal punto di vista del modello che avevo progettato, invece, aveva appena introdotto una seconda rappresentazione dello stato.

Prima avevo, concettualmente:

    stato_del_messaggio = stato_nello_spool

Dopo avevo:

    stato_del_messaggio = stato_nello_spool
                          + stato_nella_cache

e adesso dovevo anche dimostrare una proprietà nuova:

    stato_nella_cache == stato_nello_spool

ogni volta che quella uguaglianza era necessaria.

Naturalmente una cache non trasforma magicamente un automa deterministico in qualcosa che non lo è. Posso benissimo aggiungere lo stato della cache all'insieme degli stati dell'automa e modellare anche le sue transizioni.

Posso farlo.

Ma a quel punto devo anche dimostrare la coerenza della cache, l'invalidation, gli aggiornamenti, i casi di errore, il riavvio del processo, eventuali modifiche esterne e tutto ciò che deriva dall'avere due rappresentazioni della stessa informazione.

Cioè avevo ottenuto una piccola accelerazione comprandomi in cambio una quantità considerevole di stato e di invarianti da dimostrare.

Nel mio caso non ne valeva semplicemente la pena. Il filesystem e il sistema operativo fanno già caching a un livello inferiore, e non avevo un problema prestazionale tale da giustificare un secondo livello di cache applicativa con tutta la complessità di consistenza che avrebbe comportato.

Ma il punto interessante non è nemmeno la cache.

Il punto è: chi aveva deciso di mettercela?

L'agente.

Io non avevo chiesto:

“Cambia l'architettura dello spool.”

Non avevo chiesto:

“Aggiungi una seconda sorgente dello stato.”

Avevo chiesto di continuare a implementare delle funzionalità mantenendo determinate proprietà.

Solo che “se vuoi aumentare le performance, aggiungi una cache” è un pattern estremamente comune nel software che un LLM ha visto durante l'addestramento. È una soluzione plausibile, frequente, generalmente sensata e quindi statisticamente assai attraente.

Il problema è che nel mio programma violava una decisione architetturale molto più importante dell'aumento di performance che poteva ottenere.

E senza la verifica formale probabilmente non me ne sarei accorto immediatamente.

Avrei fatto qualche benchmark, avrei visto un piccolo miglioramento, avrei detto “bene”, e avrei continuato.

Poi sarebbe arrivato il traffico.

Oppure un restart.

Oppure un caso limite.

Oppure semplicemente una sequenza di eventi che rendeva le due rappresentazioni dello stato incoerenti.

GNATprove, invece, non era interessato al benchmark.

Io gli avevo chiesto di dimostrare certe proprietà e, dopo quella modifica, non riusciva più a dimostrarle.

Fine della discussione.

Ed è questa, secondo me, una delle cose più interessanti che si imparano programmando con gli agenti AI.

Un agente è estremamente bravo a produrre una soluzione plausibile.

Ma “plausibile” e “compatibile con l'architettura che avete progettato” sono due concetti completamente diversi.

E più il lavoro diventa lungo, più i vincoli diventano numerosi, più diventa pericoloso confidare nel fatto che il modello continui semplicemente a ricordarseli tutti*.

Se avete una specifica, scritta in linguaggio naturale o meno, a un certo punto l'agente può dimenticarla, reinterpretarla o sacrificarne un pezzo per applicare qualche pattern che gli sembra più conveniente. O semplicemente, statisticamente frequente.

Se invece una parte della specifica è diventata matematica, succede una cosa molto più divertente.

L'agente può dimenticarsela.

Il prover no: e' un matematico rompicoglioni che fa test. Ed e' anche un computer. Di quelli alla vecchia, tutto Von Neumann e niente spine.

---

Cosa mi ha insegnato questa esperienza?

Che gli agenti possono farvi risparmiare una quantità considerevole di tempo, ma che avere un meccanismo automatico capace di controllare quello che fanno è essenziale.

Insomma: occorre la supervisione di un umano.

Solo che, se il codice comincia a essere parecchio, e l'umano non ha una particolare ossessione per la consistenza di ventimila righe di software, la supervisione umana da sola comincia a diventare un concetto piuttosto ottimistico.

Quindi occorre anche il tool giusto.

Non a caso attorno a Rust sta crescendo un ecosistema piuttosto serio di strumenti di verifica formale: Kani, Verus, Creusot, Prusti e altri. Lo stesso progetto Rust sta lavorando alla verifica della standard library e a un sistema di contratti utilizzabile dagli strumenti di analisi formale. Non siamo ancora al livello di integrazione e maturità che SPARK ha raggiunto nel suo mondo, ma la direzione è evidente.

Anche per Go esistono verificatori formali, per esempio Gobra, anche se qui parliamo più di strumenti sviluppati attorno al linguaggio che di qualcosa che faccia parte organicamente del progetto Go.

MISRA C e famiglia sono un'altra cosa ancora: sono soprattutto insiemi di regole per restringere l'uso del C ed evitare una quantità di comportamenti pericolosi. Sono utilissimi, specialmente nel software safety-critical, ma non costituiscono di per sé una dimostrazione formale del programma.

E, personalmente, continuo a pensare che il C da questo punto di vista sia una brutta bestia.

Ma torniamo agli agenti.

Li lascerei scrivere da soli codice Ada/SPARK?

No.

Anzi: considerando gli ambienti nei quali Ada e SPARK vengono usati, MI AUGURO che nessuno lasci un agente non supervisionato a scrivere software destinato a missili, aerei, treni, navi, apparati medicali e compagnia cantante.

Sarebbe una pazzia.

Il problema è che ultimamente la frase “sarebbe una pazzia” non mi tranquillizza più come una volta.

Nel 2026 sono emersi diversi casi nei quali modelli di OpenAI e Anthropic, sottoposti a valutazioni di cybersecurity, si sono trovati ad avere accesso alla Internet pubblica mentre eseguivano compiti offensivi.

In un test del britannico AI Security Institute l'accesso a Internet era stato abilitato intenzionalmente, per rendere l'ambiente più simile a quello di un attaccante reale. In un'altra serie di test, condotta da un valutatore esterno, l'accesso alla rete pubblica era invece dovuto a una configurazione sbagliata del testbed. In almeno un caso un modello OpenAI arrivò così ad attaccare un sito reale credendolo parte dell'esercitazione.

Anthropic ha poi descritto quattro incidenti nei quali modelli Claude, durante valutazioni di cybersecurity dello stesso tipo, ebbero accesso non autorizzato a sistemi reali perché l'ambiente che avrebbe dovuto essere isolato poteva in realtà raggiungere Internet.

Quindi sì: “nessuno sarà così pazzo” ha perso un po' del suo potere rassicurante.

Per essere sintetici.

L'agente può, a mio avviso, sostituire il programmatore?

No.

È un sistema generativo, probabilistico, addestrato su enormi quantità di esempi. Può quindi proporre un pattern comunissimo, perfettamente ragionevole nella maggioranza dei programmi e catastrofico proprio nel vostro.

L'agente è inutile?

Neppure.

Può scrivere una quantità impressionante di buon codice. Può togliervi dalle scatole molto lavoro ripetitivo, implementare strutture che avete già progettato, produrre test, fare refactoring, cercare errori.

Solo che ogni tanto svirgola.

E non volete che il momento in cui svirgola coincida con quello in cui sta lavorando sul vostro missile preferito.

Se però viene adeguatamente sorvegliato, e se il progetto dispone di strumenti automatici capaci di verificare le proprietà che davvero vi interessano — test, static analysis, model checking, contratti, verifica formale, a seconda del problema — allora un agente AI può diventare uno strumento che accelera enormemente il lavoro del programmatore?

Sì.

Assolutamente.

Quindi, se mi chiedete dove metto oggi un agente AI sull'asse che va da:

    random bytes <------------------------> sostituisce un programmatore

la risposta è che non lo metto né da una parte né dall'altra.

Sta nel mezzo.

È un tool.

Un tool capace di fare moltissimo, ma insieme a un programmatore che decide l'architettura, scrive le specifiche, stabilisce quali proprietà debbano essere vere e soprattutto dispone dei mezzi necessari per verificare che lo siano davvero.

L'agente può scrivere il codice.

Qualcuno, però, deve ancora sapere che cosa quel codice deve significare.

---

E quindi cosa penso delle aziende che fanno lavorare questi agenti praticamente senza supervisione umana?

Che sono dei folli.

Perché questi agenti produrranno codice che funziona la maggior parte delle volte.

Ed è proprio questo il problema.

“La maggior parte delle volte” può essere perfettamente accettabile per generare una bozza, riordinare del testo o suggerire una funzione. Diventa molto meno rassicurante quando quel codice finisce in produzione e comincia a gestire soldi, dati, macchine, reti, processi industriali o persone.

Il software, soprattutto quello importante, non viene giudicato su quanto spesso funziona quando tutto va come previsto.

Viene giudicato su cosa succede quella volta in cui non lo fa.

E quindi sì: magari i manager risparmieranno sul costo dei programmatori.

Dormiranno anche peggio.

Perché prima o poi potrebbero scoprire, nel modo meno piacevole possibile, che cosa significa davvero:

“Funziona nella maggior parte dei casi.”