L'audit di Trail of Bits su Miden ha scoperto una falla in Falcon dopo che gli agenti hanno creato gli strumenti mancanti

Trail of Bits ha dedicato sei mesi alla preparazione dell'audit su Miden, trovando poi una falla ad alta gravità con strumenti che i suoi agenti AI avevano costruito da zero. L'audit di Trail of Bits su Miden ha richiesto ben più che puntare un modello al codice sorgente. I suoi agenti hanno creato un server LSP, un decompilatore, un motore di analisi statica e un modello Lean prima dell'inizio della revisione formale.

Quella preparazione ha rivelato un valore sottovincolato che, secondo quanto riportato, poteva consentire a un prover malevolo di falsificare firme Falcon e svuotare gli account interessati. Gli analizzatori hanno inoltre identificato più di 400 punti in cui la validazione dei tipi poteva essere migliorata. Nel frattempo, l'attività di verifica formale ha prodotto 95 prove di correttezza verificate automaticamente e ha scoperto due bug non rilevati dai test unitari esistenti.

Il confronto importante non è tra agenti AI e revisori umani. È tra una revisione diretta del codice tramite AI e la costruzione, assistita da agenti, dell'infrastruttura che rende possibile la revisione di codice complesso. Trail of Bits ha continuato a fare affidamento sulla supervisione umana, sulla revisione manuale dei teoremi e sul tradizionale giudizio di sicurezza. Gli agenti hanno cambiato quali progetti di supporto fossero economicamente praticabili.

L'audit di Trail of Bits su Miden è iniziato con sei mesi di anticipo

Il lavoro decisivo è iniziato prima che i revisori ricevessero un obiettivo finito da ispezionare.

Il team di Miden ha contattato Trail of Bits alla fine del 2025, secondo il dettagliato resoconto dell'audit su Miden pubblicato dalla società. Miden voleva che parti della sua macchina virtuale a conoscenza zero fossero sottoposte a revisione prima del lancio. Una sezione riguardava una libreria principale contenente primitive crittografiche scritte in Miden Assembly, o MASM.

Una macchina virtuale a conoscenza zero, spesso abbreviata in zkVM, dimostra che un programma è stato eseguito correttamente senza richiedere a ogni verificatore di ripetere quel calcolo. Miden utilizza un'architettura a macchina a pila. Le istruzioni consumano valori da una pila e vi reinseriscono i risultati.

Quell'architettura conta perché input e output sono spesso impliciti nel codice MASM. Un revisore deve seguire come ogni istruzione modifica la pila, quindi trasferire quello stato attraverso rami, cicli e chiamate di procedura. I consueti indizi a livello di sorgente possono scomparire.

MASM mancava inoltre di gran parte degli strumenti che i revisori normalmente si aspettano. Il supporto dell'editor era limitato, non esisteva un language server maturo pensato per la revisione e l'analisi automatizzata della libreria principale era ridotta. Trail of Bits sapeva che l'implementazione non era ancora completa di tutte le funzionalità, ma sapeva anche che la revisione sarebbe avvenuta sei mesi dopo.

La società ha sfruttato quella finestra temporale per costruire il proprio ambiente di revisione. Claude ha prodotto un prototipo iniziale di language server in pochi giorni, afferma Trail of Bits. Il risultante MASM language server offre navigazione, individuazione dei riferimenti, documentazione al passaggio del mouse, diagnostica della sintassi, descrizioni delle istruzioni e informazioni sugli effetti sulla pila.

Queste funzionalità sembrano normali comodità per gli sviluppatori. In un linguaggio assembly poco familiare, diventano parte del metodo di sicurezza. La navigazione aiuta i revisori a tracciare un valore oltre i confini delle procedure. Gli effetti sulla pila visualizzati inline riducono le ripetute ricostruzioni manuali. La diagnostica espone le ipotesi prima che si trasformino in rilievi.

Trail of Bits ha poi esteso il progetto alla decompilazione, all'analisi statica, agli strumenti da riga di comando e alla modellazione formale. Claude ha gestito attività di pianificazione e implementazione, mentre Codex ha partecipato alla revisione del codice. Gli agenti hanno inoltre alternato i ruoli, sottoponendo il lavoro generato a un passaggio di revisione separato.

Non si è trattato di un processo di generazione una tantum. Dopo aver implementato una funzionalità, il team ha chiesto agli agenti di decompilare procedure casuali e confrontare i risultati con il MASM originale. Le regressioni sono diventate test, e il modello ha poi lavorato rispetto a tali test.

Questo ciclo di feedback è centrale nella vicenda. Gli agenti non sono stati trattati come autorità il cui output meritasse fiducia automatica. Operavano all'interno di un sistema di verifica in crescita che comprendeva test, fasi di revisione, analizzatori e, in seguito, un verificatore di prove.

L'audit è quindi iniziato da una domanda diversa rispetto a quella abituale. Trail of Bits non ha chiesto soltanto se un agente potesse trovare vulnerabilità. Ha chiesto quali strumenti mancanti impedissero ai revisori, compresi gli agenti, di comprendere il codice in primo luogo.

Questo cambiamento di portata ha creato le condizioni per le conclusioni successive. Ha inoltre esercitato pressione sui team di sicurezza che promuovono la revisione con AI soprattutto come una scansione più rapida del codice sorgente. L'approccio di Trail of Bits ha richiesto maggiore preparazione, ma ha convertito quella preparazione in infrastruttura tecnica riutilizzabile.

Il decompilatore è diventato più prezioso del suo output

Il decompilatore contava soprattutto perché la sua rappresentazione interna offriva alle altre analisi un luogo affidabile in cui operare.

Decompilare MASM non significava semplicemente sostituire le istruzioni assembly con espressioni leggibili. La maggior parte delle procedure della libreria principale non disponeva di firme dichiarate, quindi gli strumenti dovevano spesso dedurne input e output dal contesto. Le procedure mancavano inoltre di una convenzione di chiamata uniforme.

I cicli creavano un altro problema. Un ciclo while in MASM non deve necessariamente preservare la stessa forma della pila tra un'iterazione e l'altra. La sua condizione può spostarsi in un'altra posizione della pila, compromettendo i semplici tentativi di assegnare nomi stabili agli input delle istruzioni.

Anche i rami condizionali possono produrre effetti diversi sulla pila. Se un ramo aggiunge un elemento mentre un altro ne rimuove uno, il decompilatore non può unire ciecamente i loro stati. Gli errori nell'inferenza degli effetti sulla pila possono quindi propagarsi attraverso ogni procedura che chiama il codice interessato.

Trail of Bits ha risposto limitando la propria promessa. Il suo decompilatore MASM si rivolge a un sottoinsieme ben definito invece di dichiarare un recupero perfetto per ogni procedura. Questa scelta ha privilegiato la correttezza rispetto a una copertura superficiale.

Il decompilatore è diventato il maggiore sforzo di sviluppo degli strumenti nel progetto. Trail of Bits riferisce di oltre 100 commit generati dall'AI nell'arco di diversi mesi. Eppure lo pseudocodice finale non è stato il suo output più rilevante.

Il progetto ha creato una rappresentazione intermedia, o IR, che esprimeva input e output delle procedure come espressioni analizzabili. Un'IR è una versione strutturata del codice progettata per la trasformazione o l'analisi. Una volta che le istruzioni MASM sono esistite in quella forma, il team ha potuto applicare consolidate tecniche di flusso dei dati e analisi statica.

L'analizzatore poteva chiedere se i valori forniti dal prover fossero validati prima dell'uso. Poteva tracciare se il codice imponesse i tipi previsti, come interi a 32 bit o valori Booleani. Poteva inoltre determinare se le variabili locali fossero inizializzate lungo ogni possibile percorso di esecuzione.

Trail of Bits ha utilizzato l'interpretazione astratta per una parte di questo lavoro. L'interpretazione astratta valuta categorie di possibili valori invece di eseguire un programma con un singolo input concreto. Un valore potrebbe essere rappresentato come un intero valido a 32 bit, un Booleano o un valore sconosciuto.

L'analisi si ripete finché non raggiunge uno stato stabile in cui non emergono nuove informazioni. Se progettata in modo solido, sovrastima ciò che le esecuzioni reali possono fare. Questo può produrre falsi positivi, ma non dovrebbe escludere silenziosamente un comportamento reale coperto dal modello.

Questo dimostra perché l'audit di Trail of Bits su Miden differisce da una generica dimostrazione di programmazione con AI. Il decompilatore generato dagli agenti non è stato considerato affidabile per dichiarare sicuro il codice. Ha contribuito a costruire un substrato sul quale potevano essere eseguite analisi esplicite e ispezionabili.

Il flusso di lavoro ha creato vantaggi anche per gli esseri umani. Le procedure decompilate hanno reso più semplice rivedere il flusso di controllo e dei dati ad alto livello direttamente nell'editor. Le annotazioni della pila hanno ridotto il lavoro mentale di tracciamento. Le interfacce da riga di comando hanno reso le stesse capacità disponibili ai processi di revisione automatizzati.

C'è una lezione più ampia per i team che valutano gli agenti di programmazione. L'artefatto generato più prezioso potrebbe non essere quello che gli utenti vedono. Un decompilatore con un ambito parziale può comunque giustificare il proprio costo se il suo parser, il modello di flusso di controllo e l'IR sbloccano numerosi controlli di valore più elevato.

Questa conclusione cambia anche il modo in cui i team dovrebbero preservare il contesto del progetto. Prompt degli agenti, casi di regressione, decisioni architetturali e commenti dei revisori diventano input ingegneristici durevoli. Una base di conoscenza ricercabile può contribuire a mantenere disponibili questi materiali durante progetti di sicurezza di lunga durata.

La revisione diretta con AI di solito parte dal codice target e cerca difetti. Trail of Bits ha invece utilizzato gli agenti per modificare la superficie di revisione. Il risultato successivo ha mostrato perché questa distinzione contava.

Un controllo mancante ha raggiunto l'autenticazione Falcon

Un singolo resto non validato avrebbe trasformato un helper aritmetico in un percorso per falsificare l'autenticazione.

Durante l'audit, le analisi statiche hanno identificato più di 400 posizioni uniche in cui la validazione dei tipi poteva essere migliorata. Trail of Bits afferma che tutte erano raggiungibili dall'API pubblica della libreria principale. Molte derivavano dal fatto che le procedure esposte pubblicamente potevano essere chiamate senza le ipotesi previste dai loro autori originari.

Una procedura pubblica non può fare affidamento in modo sicuro sul fatto che ogni chiamante fornisca un valore del tipo previsto. In un sistema di prove, è particolarmente importante distinguere un valore fornito dal prover da un valore vincolato dalla prova. Il semplice inserimento di dati in un calcolo non stabilisce che rappresentino l'intero o il Booleano dichiarato.

Il rilievo ad alta gravità si è concentrato su mod_12289, una procedura che riduce un valore a 64 bit modulo 12.289. Il prover forniva un quoziente e un resto attraverso un meccanismo di advice. I valori advice sono suggerimenti di esecuzione calcolati al di fuori della VM, spesso usati per evitare costose elaborazioni nella VM.

Il quoziente riceveva un controllo che confermava la sua conformità alla rappresentazione prevista a 64 bit. Il resto non riceveva una validazione equivalente prima di entrare in u32overflowing_sub, un'istruzione di sottrazione a 32 bit.

Trail of Bits afferma che un attaccante poteva variare quoziente e resto continuando a soddisfare i vincoli della sottrazione. Ciò consentiva a mod_12289 di restituire qualcosa di diverso dal resto matematicamente corretto.

La portata del bug andava oltre un risultato aritmetico errato. La procedura supportava la verifica delle firme Falcon. Falcon è uno schema di firma digitale post-quantistica, e Miden ne utilizzava una variante per l'autenticazione degli account.

Secondo Trail of Bits, un prover malevolo poteva sfruttare il valore sottovincolato per falsificare una firma Falcon e svuotare un account controllato da una coppia di chiavi Falcon. Questa è l'affermazione tecnica della società, non un exploit riprodotto indipendentemente e presentato nell'articolo pubblico.

La gravità deriva dal modello di esecuzione di Miden. Il design della Miden VM supporta input non deterministici forniti durante la generazione della prova. Questi input possono migliorare l'efficienza, ma il programma deve vincolarli con attenzione.

Un verificatore non deduce l'intenzione dello sviluppatore. Controlla se la prova presentata soddisfa i vincoli codificati. Se tali vincoli accettano un resto non valido, la prova può rimanere valida anche quando la relazione aritmetica dichiarata è falsa.

Questo è il capovolgimento fondamentale. Le prove a conoscenza zero possono stabilire l'esecuzione fedele di un sistema specificato, ma non possono riparare una specifica incompleta. Una prova crittografica di un programma sottovincolato può fornire fiducia nella proprietà sbagliata.

Il contesto indipendente di un successivo audit dei contratti Miden rafforza il punto generale. OpenZeppelin ha descritto le transazioni Miden come valide quando esiste una prova corrispondente, rendendo ogni controllo MASM parte dei vincoli che un prover deve soddisfare.

Questo incarico separato riguardava un diverso ambito di repository e non va confuso con la revisione di Trail of Bits. Tuttavia, entrambe le analisi mostrano perché la logica di autenticazione, gli input controllati dal prover e le assunzioni on-chain richiedano un trattamento esplicito.

Anche le oltre 400 posizioni di validazione dei tipi vanno interpretate con cautela. Non sono state descritte come 400 vulnerabilità sfruttabili. Rappresentavano punti in cui la validazione poteva essere migliorata, tra cui una vulnerabilità segnalata ad alta gravità.

Questa distinzione è importante perché l'analisi statica spesso individua condizioni che richiedono triage. Un analizzatore affidabile può intenzionalmente segnalare più casi di quelli che alla fine si trasformano in difetti di sicurezza. Il suo valore risiede nell'individuare sistematicamente le assunzioni che meritano un esame.

Per i team di sicurezza, il risultato mette sotto pressione una scorciatoia comune: usare un agente per riassumere funzioni sospette senza prima modellare le regole di valore del linguaggio di destinazione. Un modello può spiegare cosa il codice sembra fare. L'analizzatore può chiedere se ogni esecuzione consentita rispetti effettivamente il tipo richiesto.

La scoperta di Falcon è nata dalla combinazione di entrambe le capacità. Gli agenti hanno accelerato la costruzione, mentre la semantica statica ha trasformato un'intuizione sui dati controllati dal prover in un controllo ripetibile.

Le prove Lean hanno individuato ciò che i test unitari non vedevano

La verifica formale non ha sostituito i test, ma ha costretto il team a definire il comportamento con una precisione sufficiente a far emergere due errori mai testati.

Trail of Bits ha perseguito la modellazione formale anche dopo aver realizzato gli strumenti per editor e analisi statica. La domanda era volutamente diversa: se una procedura di libreria non conteneva difetti evidenti, il team poteva dimostrare che la sua implementazione corrispondeva al comportamento aritmetico previsto?

L'azienda ha realizzato un esecutore minimale della Miden VM in Lean. Lean è un theorem prover interattivo il cui piccolo kernel affidabile verifica se una prova inviata deriva dalle sue definizioni e assunzioni. Claude ha inoltre contribuito a realizzare un traduttore dalle procedure MASM alle rappresentazioni Lean.

Più agenti hanno quindi lavorato in parallelo alle prove delle procedure. Il risultante modello Lean di MASM contiene semantica eseguibile della VM, procedure tradotte, supporto condiviso alle prove e singoli teoremi di correttezza.

Il repository elenca 95 prove di procedure verificate: 31 per operazioni a 64 bit, 36 per operazioni a 128 bit, 17 per operazioni a 256 bit e 11 per operazioni sulle word. Insieme, coprono le parti di aritmetica binaria descritte da Trail of Bits.

Non erano prove che ogni parte di Miden fosse sicura. Riguardavano proprietà di correttezza definite per procedure specifiche. Questo confine è essenziale perché un theorem prover verifica il teorema che gli viene fornito, non l'intento non dichiarato nella mente di uno sviluppatore.

Trail of Bits afferma che i revisori umani si sono quindi concentrati sull'audit degli enunciati dei teoremi. Se un agente avesse dimostrato un teorema che ometteva una precondizione critica o esprimeva il risultato sbagliato, la sola accettazione del kernel non avrebbe reso corretto il software.

A un livello generale, molti teoremi seguivano uno schema riconoscibile. Data una pila con input specifici, l'esecuzione di una procedura dovrebbe terminare e lasciare in cima il risultato matematicamente atteso. I valori della pila non correlati e di proprietà del chiamante dovrebbero rimanere nelle posizioni previste.

Questa pressione sulla specifica ha fatto emergere due difetti sfuggiti ai test unitari esistenti. Il primo riguardava una procedura di rotazione a destra a 64 bit chiamata rotr. Si comportava in modo errato per input grandi superiori al primo di Goldilocks quando l'ammontare della rotazione era un multiplo di 32.

Il primo di Goldilocks definisce il campo usato dalla VM, quindi i valori prossimi o superiori a quel limite richiedono una rappresentazione accurata. Durante il lavoro sulle prove, il teorema desiderato non poteva essere dimostrato senza aggiungere un'assunzione che escludesse il caso problematico di shift.

Una prova fallita non è automaticamente prova di un bug nel codice. Anche il teorema, il modello o i lemmi di supporto possono essere errati. In questo caso, la revisione manuale dell'ostacolo ha portato il team al caso limite nell'implementazione.

Il secondo bug è comparso nella procedura wrapping_mul a 256 bit. Trail of Bits afferma che rimuoveva dalla pila, prima del ritorno, valori di proprietà del chiamante. I normali test del risultato della moltiplicazione potevano superare il controllo senza verificare la preservazione dello stato circostante della pila.

Quel difetto mostra perché le postcondizioni precise siano importanti. Una procedura può calcolare la risposta numerica corretta violando al contempo il proprio contratto di chiamata. In una stack machine, danneggiare lo stato adiacente può influire sull'esecuzione successiva anche quando l'elemento in cima appare corretto.

I test unitari mantengono comunque un ruolo centrale. Vengono eseguiti rapidamente, proteggono dalle regressioni note e coprono comportamenti di integrazione che potrebbero non avere ancora un modello formale. Lo sforzo Lean ha fornito un tipo diverso di garanzia su proprietà dichiarate esplicitamente.

Il vantaggio chiave era composizionale. Gli agenti potevano produrre tentativi di prova su larga scala, mentre il kernel di Lean rifiutava le derivazioni non valide. Gli esseri umani non dovevano fidarsi della sicurezza espressa in prosa da un modello. Dovevano esaminare le definizioni e confermare che i teoremi accettati rappresentassero le garanzie previste.

Questo è un confine di controllo più solido che chiedere a un altro modello linguistico se il codice generato sembri corretto. Non elimina il giudizio umano, ma sposta quel giudizio verso specifiche e assunzioni.

Per i responsabili dell'ingegneria, il caso suggerisce una pratica divisione del lavoro. Gli agenti possono generare infrastrutture ripetitive per le prove, traduttori e lemmi candidati. Gli specialisti umani decidono cosa debba essere dimostrato e indagano perché enunciati importanti falliscano.

Il risultato non rende affidabili gli audit autonomi

Il progetto supporta l'ingegneria degli audit assistita da agenti, non la certificazione della sicurezza senza supervisione.

Trail of Bits inquadra direttamente il cambiamento economico. Solo pochi anni prima, avrebbe faticato a giustificare mesi di strumenti esplorativi per un singolo incarico. Progetti collaterali di questo tipo avevano risultati incerti ed erano difficili da vendere prima che il loro valore diventasse visibile.

L'azienda sostiene che gli agenti abbiano ridotto abbastanza il costo dell'esplorazione da cambiare questo calcolo. Gli esperimenti falliti costano sempre più token e tempo di supervisione anziché un'allocazione completa di lavoro ingegneristico specialistico.

Questa affermazione merita una lettura attenta. Sono comunque trascorsi sei mesi prima dell'audit e il solo decompilatore ha accumulato più di 100 commit generati dall'AI. Il resoconto pubblico non fornisce un confronto controllato tra ore del personale, costi totali dei modelli o rendimento in difetti rispetto a un incarico convenzionale.

Non dimostra nemmeno che gli agenti possano realizzare strumenti equivalenti per ogni linguaggio insolito. MASM offriva proprietà favorevoli all'analisi e alla modellazione formale. La Miden VM ha un set di istruzioni compatto e molte operazioni evitano effetti collaterali complessi.

Anche con questo target favorevole, il decompilatore non poteva coprire in sicurezza ogni procedura. Trail of Bits ha ristretto il sottoinsieme supportato perché effetti sulla pila incoerenti e firme mancanti rendevano impraticabile una decompilazione completa e affidabile.

Il flusso di lavoro Lean comportava un altro limite. Le prove verificate dal kernel stabiliscono solo il teorema dichiarato secondo la semantica modellata. Un'istruzione tradotta erroneamente, un modello VM incompleto o un teorema debole possono mantenere un divario tra il comportamento dimostrato e il deployment reale.

La revisione umana è rimasta visibile durante tutto il processo. Gli auditor hanno revisionato il codice generato dagli agenti, trasformato le regressioni in test, ispezionato gli enunciati dei teoremi e analizzato le prove fallite. Claude e Codex si sono alternati tra sviluppo e revisione anziché operare come un'autorità non osservata.

Questo rende più netto il confronto principale. La revisione diretta con l'AI chiede a un modello di riconoscere vulnerabilità in una rappresentazione esistente. Gli agenti che costruiscono strumenti aiutano gli esperti a creare una rappresentazione in cui vincoli mancanti, tipi non validi e postcondizioni errate diventano espliciti.

Nessuno dei due approcci dovrebbe essere adottato isolatamente. I modelli possono far emergere ipotesi che gli analizzatori statici non codificano. L'analisi statica può coprire percorsi di esecuzione che un revisore probabilistico potrebbe trascurare. La prova formale può quindi affrontare proprietà selezionate con uno standard verificabile dalla macchina.

Il processo crea anche obblighi di manutenzione. I parser devono seguire i cambiamenti del linguaggio. Gli analizzatori necessitano di suite di regressione. I modelli formali devono rimanere allineati alla semantica della VM. Strumenti generati che diventano obsoleti possono creare una falsa garanzia.

Trail of Bits riferisce che il team Miden ha adottato il motore di analisi statica per i futuri aggiornamenti della libreria core. È un segnale importante perché porta gli strumenti oltre l'istantanea di un singolo audit. L'uso continuativo verificherà se l'analizzatore rimarrà utile man mano che linguaggio e libreria evolvono.

Le organizzazioni che valutano un flusso di lavoro simile dovrebbero inoltre pianificare la provenienza. I team devono sapere quale modello ha generato una modifica, quale persona l'ha revisionata, quali test sono stati eseguiti e quali assunzioni sono entrate in una prova. Un flusso di lavoro ingegneristico è verificabile solo quanto lo sono le registrazioni conservate attorno a esso.

Le prove pubbliche supportano quindi una conclusione circoscritta. Gli agenti hanno reso fattibile un ambizioso programma di preparazione per questo incarico. La garanzia di sicurezza derivava comunque dal sistema combinato di esperti di dominio, test, analisi esplicite e verifica delle prove.

Questo sistema è più interessante dell'affermazione secondo cui un'AI ha trovato un bug. Offre un modello concreto per utilizzare agenti imperfetti senza trattare la loro sicurezza come una prova.

Tre segnali verificheranno se questo modello di audit durerà

Il prossimo banco di prova è stabilire se gli strumenti di garanzia costruiti dagli agenti rimarranno corretti, adottati e produttivi dopo i risultati di maggiore richiamo.

Il primo segnale è la continua integrazione dell'analizzatore MASM nel processo di sviluppo di Miden. Trail of Bits afferma che il team Miden ha adottato il motore di analisi statica per i futuri cambiamenti della libreria core. L'uso di routine nell'integrazione continua rafforzerebbe l'argomento secondo cui gli strumenti di audit possono diventare infrastruttura preventiva.

La misura importante non è il numero di avvisi emessi. È se le nuove procedure pubbliche ricevano la validazione richiesta prima del rilascio e se gli aggiornamenti dell'analizzatore seguano i cambiamenti nella semantica MASM. Falsi positivi persistenti o modelli obsoleti indebolirebbero il risultato.

Il secondo segnale è l'espansione e la manutenzione delle 95 prove Lean. Ulteriori procedure verificate mostrerebbero che il modello iniziale supporta il lavoro continuo anziché una dimostrazione fissa. Le modifiche al codice aritmetico esistente dovrebbero inoltre attivare aggiornamenti o fallimenti delle prove.

Osservate il confine tra codice tradotto e specifiche revisionate manualmente. Un'automazione che espanda il conteggio delle prove senza rafforzare la copertura dei teoremi non fornirebbe la stessa garanzia. Una documentazione chiara delle assunzioni sarà importante quanto il totale grezzo.

Il terzo segnale è la replica da parte di altri team di audit e altri ecosistemi di linguaggi. Miden presentava una combinazione insolitamente adatta: un linguaggio personalizzato, strumenti mancanti, semantica delle prove esplicita e mesi di tempo di preparazione.

Uno schema ripetuto tra diverse zkVM o linguaggi di basso livello sosterrebbe l'affermazione economica più ampia di Trail of Bits. L'impossibilità di riprodurlo su sistemi con concorrenza, memoria complessa o grandi grafi di dipendenze ne rivelerebbe i limiti.

L'audit Miden di Trail of Bits ha già prodotto più di un flusso di lavoro speculativo. Ha fornito un'integrazione per editor, un decompilatore, un analizzatore, un modello VM, prove verificate e risultati concreti sulla sicurezza.

La domanda duratura è se i team riescano a mantenere tali artefatti allineati ai sistemi che proteggono. Gli sviluppatori che valutano la sicurezza assistita da agenti dovrebbero esaminare i repository, verificare le ipotesi modellate e chiedersi dove controlli verificabili automaticamente sostituiscano la fiducia nel modello. Questo è lo standard da portare con sé nel prossimo audit.