L’audit Miden de Trail of Bits a révélé une faille Falcon après que des agents ont créé les outils manquants

Trail of Bits a consacré six mois à préparer l’audit de Miden, avant d’identifier une faille de haute gravité à l’aide d’outils que ses agents IA avaient créés de toutes pièces. L’audit Miden de Trail of Bits ne s’est pas limité à soumettre le code source à un modèle. Ses agents ont créé un serveur LSP, un décompilateur, un moteur d’analyse statique et un modèle Lean avant le début de l’examen formel.

Cette préparation a mis au jour une valeur insuffisamment contrainte qui aurait, selon les informations rapportées, permis à un prouveur malveillant de forger des signatures Falcon et de vider les comptes concernés. Les analyseurs ont également identifié plus de 400 emplacements où la validation des types pouvait être améliorée. Parallèlement, l’effort de vérification formelle a produit 95 preuves de correction vérifiées par machine et révélé deux bugs non détectés par les tests unitaires existants.

L’enjeu majeur n’oppose pas les agents IA aux auditeurs humains. Il oppose l’examen direct du code par IA à la construction, assistée par agents, de l’infrastructure qui rend possible l’examen de code complexe. Trail of Bits s’est toujours appuyé sur une supervision humaine, une revue manuelle des théorèmes et un jugement de sécurité conventionnel. Les agents ont modifié les projets de soutien qui étaient économiquement réalisables.

L’audit Miden de Trail of Bits a commencé six mois plus tôt

Le travail décisif a commencé avant même que les auditeurs ne reçoivent une cible finalisée à examiner.

L’équipe Miden a contacté Trail of Bits à la fin de 2025, selon le récit détaillé de l’entreprise sur l’audit Miden. Miden souhaitait faire examiner certaines parties de sa machine virtuelle à divulgation nulle de connaissance avant son lancement. L’une d’elles concernait une bibliothèque centrale contenant des primitives cryptographiques écrites en Miden Assembly, ou MASM.

Une machine virtuelle à divulgation nulle de connaissance, souvent abrégée en zkVM, prouve qu’un programme a été exécuté correctement sans obliger chaque vérificateur à reproduire ce calcul. Miden utilise une architecture de machine à pile. Les instructions consomment des valeurs d’une pile et y replacent leurs résultats.

Cette architecture compte, car les entrées et sorties sont souvent implicites dans le code MASM. Un relecteur doit suivre la manière dont chaque instruction modifie la pile, puis conserver cet état à travers les branches, les boucles et les appels de procédure. Les repères familiers du code source peuvent disparaître.

MASM ne disposait pas non plus d’une grande partie des outils que les auditeurs attendent habituellement. Le support dans les éditeurs était limité, il n’existait pas de serveur de langage mature adapté à l’audit, et l’analyse automatisée de la bibliothèque centrale restait restreinte. Trail of Bits savait que l’implémentation n’était pas encore complète sur le plan fonctionnel, mais savait aussi que l’examen aurait lieu six mois plus tard.

L’entreprise a utilisé cette période pour créer son propre environnement d’audit. Claude a produit un premier prototype de serveur de langage en quelques jours, indique Trail of Bits. Le serveur de langage MASM qui en a résulté fournit la navigation, la découverte de références, la documentation au survol, les diagnostics de syntaxe, les descriptions d’instructions et les informations sur les effets sur la pile.

Ces fonctionnalités peuvent sembler être de simples commodités pour développeurs. Dans un langage d’assemblage inconnu, elles deviennent une partie de la méthode de sécurité. La navigation aide les auditeurs à suivre une valeur au-delà des frontières entre procédures. Les effets de pile intégrés réduisent les reconstructions manuelles répétées. Les diagnostics révèlent les hypothèses avant qu’elles ne se transforment en constats.

Trail of Bits a ensuite étendu le projet au désassemblage, à l’analyse statique, aux outils en ligne de commande et à la modélisation formelle. Claude a pris en charge les tâches de planification et d’implémentation, tandis que Codex a participé à la revue du code. Les agents ont également échangé leurs rôles, offrant au travail généré une passe de revue distincte.

Il ne s’agissait pas d’un processus de génération ponctuel. Après avoir implémenté une fonctionnalité, l’équipe a demandé aux agents de décompiler des procédures aléatoires et de comparer les résultats au MASM d’origine. Les régressions sont devenues des tests, et le modèle a ensuite travaillé en fonction de ces tests.

Cette boucle de retour est au cœur de l’histoire. Les agents n’ont pas été traités comme des autorités dont les résultats méritaient une confiance automatique. Ils opéraient au sein d’un système de vérification en expansion, comprenant des tests, des étapes de revue, des analyseurs et, plus tard, un vérificateur de preuves.

L’audit a donc commencé avec une question différente de la question habituelle. Trail of Bits ne s’est pas seulement demandé si un agent pouvait détecter des vulnérabilités. L’entreprise a cherché à déterminer quels instruments manquants empêchaient les auditeurs, y compris les agents, de comprendre le code en premier lieu.

Ce changement de périmètre a créé les conditions des constats ultérieurs. Il a également mis sous pression les équipes de sécurité qui présentent principalement l’audit par IA comme une analyse plus rapide du code source. L’approche de Trail of Bits exigeait davantage de préparation, mais elle a transformé cette préparation en infrastructure technique réutilisable.

Le décompilateur est devenu plus précieux que son résultat

Le décompilateur comptait surtout parce que sa représentation interne offrait aux autres analyses un socle fiable sur lequel s’exécuter.

Décompiler MASM ne consistait pas simplement à remplacer les instructions d’assemblage par des expressions lisibles. La plupart des procédures de la bibliothèque centrale n’avaient pas de signatures déclarées, de sorte que les outils devaient souvent déduire leurs entrées et sorties à partir du contexte. Les procédures ne disposaient pas non plus d’une convention d’appel uniforme.

Les boucles posaient un autre problème. Une boucle while MASM n’est pas obligée de préserver la même forme de pile entre les itérations. Sa condition peut se déplacer vers une autre position de pile, faisant échouer les tentatives simples d’attribuer des noms stables aux entrées des instructions.

Les branches conditionnelles peuvent également produire des effets différents sur la pile. Si une branche ajoute un élément tandis qu’une autre en retire un, le décompilateur ne peut pas fusionner aveuglément leurs états. Des erreurs dans l’inférence des effets sur la pile peuvent alors se propager à travers chaque procédure qui appelle le code concerné.

Trail of Bits a répondu en limitant sa promesse. Son décompilateur MASM cible un sous-ensemble bien défini plutôt que de prétendre récupérer parfaitement chaque procédure. Ce choix a privilégié la correction à une couverture superficielle.

Le décompilateur est devenu l’effort d’outillage le plus important du projet. Trail of Bits fait état de plus de 100 commits générés par IA sur plusieurs mois. Pourtant, le pseudo-code final n’en était pas le résultat le plus déterminant.

Le projet a créé une représentation intermédiaire, ou IR, qui exprimait les entrées et sorties des procédures sous forme d’expressions analysables. Une IR est une version structurée du code conçue pour la transformation ou l’analyse. Une fois les instructions MASM disponibles sous cette forme, l’équipe a pu appliquer des techniques établies d’analyse de flux de données et d’analyse statique.

L’analyseur pouvait vérifier si des valeurs fournies par le prouveur étaient validées avant leur utilisation. Il pouvait suivre si le code appliquait les types attendus, tels que des entiers 32 bits ou des valeurs booléennes. Il pouvait aussi déterminer si les variables locales étaient initialisées sur tous les chemins d’exécution possibles.

Trail of Bits a utilisé l’interprétation abstraite pour une partie de ce travail. L’interprétation abstraite évalue des catégories de valeurs possibles plutôt que d’exécuter un programme avec une entrée concrète unique. Une valeur peut être représentée comme un entier 32 bits valide, un booléen ou une valeur inconnue.

L’analyse se répète jusqu’à atteindre un état stable dans lequel aucune nouvelle information n’apparaît. Lorsqu’elle est conçue de manière saine, elle surapproxime ce que les exécutions réelles peuvent faire. Cela peut produire des faux positifs, mais ne devrait pas exclure silencieusement un comportement réel couvert par le modèle.

Cela illustre pourquoi l’audit Miden de Trail of Bits diffère d’une démonstration générique de programmation par IA. Le décompilateur généré par l’agent n’a pas été considéré comme fiable pour déclarer le code sûr. Il a contribué à construire un substrat sur lequel des analyses explicites et inspectables pouvaient s’exécuter.

Le flux de travail a également bénéficié aux humains. Les procédures décompilées facilitaient l’examen du contrôle de haut niveau et du flux de données dans l’éditeur. Les annotations de pile réduisaient la charge mentale de suivi. Les interfaces en ligne de commande rendaient les mêmes capacités accessibles aux processus d’audit automatisés.

Il en ressort une leçon plus large pour les équipes évaluant les agents de programmation. L’artefact généré le plus utile n’est peut-être pas celui que voient les utilisateurs. Un décompilateur au périmètre partiel peut néanmoins justifier son coût si son analyseur, son modèle de flux de contrôle et son IR ouvrent la voie à plusieurs contrôles de plus grande valeur.

Cette conclusion modifie également la manière dont les équipes doivent préserver le contexte du projet. Les prompts des agents, les cas de régression, les décisions d’architecture et les commentaires des relecteurs deviennent des apports d’ingénierie durables. Une base de connaissances consultable peut aider à maintenir ces éléments disponibles tout au long de projets de sécurité de longue durée.

L’audit direct par IA commence généralement par le code cible et recherche des défauts. Trail of Bits a plutôt utilisé les agents pour modifier la surface d’examen. Le résultat suivant a montré pourquoi cette distinction comptait.

Une vérification manquante a atteint l’authentification Falcon

Un seul reste non validé aurait transformé un auxiliaire arithmétique en voie vers une authentification falsifiée.

Au cours de l’audit, les analyses statiques ont identifié plus de 400 emplacements uniques où la validation des types pouvait être améliorée. Trail of Bits indique que tous étaient accessibles depuis l’API publique de la bibliothèque centrale. Beaucoup découlaient du fait que des procédures exposées publiquement pouvaient être appelées sans les hypothèses attendues par leurs auteurs d’origine.

Une procédure publique ne peut pas compter en toute sécurité sur le fait que chaque appelant fournira une valeur du type prévu. Dans un système de preuve, il est particulièrement important de distinguer une valeur fournie par le prouveur d’une valeur contrainte par la preuve. Le simple fait d’introduire des données dans un calcul n’établit pas qu’elles représentent l’entier ou le booléen revendiqué.

La découverte de haute gravité concernait mod_12289, une procédure qui réduit une valeur 64 bits modulo 12 289. Le prouveur fournissait un quotient et un reste via un mécanisme d’advice. Les valeurs d’advice sont des indications d’exécution calculées en dehors de la VM, souvent utilisées pour éviter des opérations coûteuses au sein de la VM.

Le quotient faisait l’objet d’une vérification confirmant qu’il correspondait à la représentation 64 bits attendue. Le reste ne recevait pas de validation équivalente avant d’entrer dans u32overflowing_sub, une instruction de soustraction 32 bits.

Trail of Bits affirme qu’un attaquant pouvait faire varier le quotient et le reste tout en satisfaisant les contraintes de soustraction. Cela permettait à mod_12289 de renvoyer autre chose que le reste mathématiquement correct.

La portée du bug allait au-delà d’un résultat arithmétique erroné. La procédure contribuait à la vérification des signatures Falcon. Falcon est un schéma de signature numérique post-quantique, et Miden utilisait une variante pour l’authentification des comptes.

Selon Trail of Bits, un prouveur malveillant pouvait exploiter la valeur insuffisamment contrainte afin de forger une signature Falcon et de vider un compte contrôlé par une paire de clés Falcon. Il s’agit de l’affirmation technique de l’entreprise, et non d’un exploit reproduit indépendamment présenté dans l’article public.

La gravité découle du modèle d’exécution de Miden. La conception de la Miden VM prend en charge des entrées non déterministes fournies lors de la génération de preuves. Ces entrées peuvent améliorer l’efficacité, mais le programme doit les contraindre avec soin.

Un vérificateur ne déduit pas l’intention du développeur. Il vérifie si la preuve soumise satisfait les contraintes encodées. Si ces contraintes acceptent un reste invalide, la preuve peut rester valide même lorsque la relation arithmétique revendiquée est fausse.

C’est le renversement central. Les preuves à divulgation nulle de connaissance peuvent établir l’exécution fidèle d’un système spécifié, mais elles ne peuvent pas réparer une spécification incomplète. Une preuve cryptographique d’un programme insuffisamment contraint peut inspirer confiance dans la mauvaise propriété.

Le contexte indépendant d’un audit ultérieur de contrats Miden renforce le constat général. OpenZeppelin a décrit les transactions Miden comme valides lorsqu’une preuve correspondante existe, faisant de chaque vérification MASM une partie des contraintes qu’un prouveur doit satisfaire.

Cette mission distincte couvrait un périmètre de dépôt différent et ne doit pas être confondue avec l’examen de Trail of Bits. Toutefois, les deux récits montrent pourquoi la logique d’authentification, les entrées contrôlées par le prouveur et les hypothèses on-chain nécessitent un traitement explicite.

Les plus de 400 emplacements de validation de type doivent également être interprétés avec prudence. Ils n’ont pas été présentés comme 400 vulnérabilités exploitables. Ils représentaient des endroits où la validation pouvait être améliorée, parmi lesquels figurait un problème signalé de gravité élevée.

Cette distinction importe, car l’analyse statique détecte souvent des conditions nécessitant un triage. Un analyseur fiable peut délibérément signaler davantage de cas que ceux qui deviendront finalement des failles de sécurité. Sa valeur réside dans l’identification systématique des hypothèses qui méritent une inspection.

Pour les équipes de sécurité, le résultat remet en question un raccourci fréquent : utiliser un agent pour résumer des fonctions suspectes sans d’abord modéliser les règles de valeurs du langage cible. Un modèle peut expliquer ce que le code semble faire. L’analyseur peut demander si chaque exécution autorisée respecte réellement le type requis.

La découverte de Falcon est venue de la combinaison de ces deux capacités. Les agents ont accéléré la construction, tandis que la sémantique statique a transformé une intuition sur des données contrôlées par le prouveur en vérification reproductible.

Les preuves Lean ont révélé ce que les tests unitaires n’avaient pas détecté

La vérification formelle n’a pas remplacé les tests, mais elle a forcé l’équipe à exprimer le comportement avec suffisamment de précision pour révéler deux échecs non testés.

Trail of Bits a poursuivi la modélisation formelle même après avoir développé les outils d’édition et d’analyse statique. La question était délibérément différente : si une procédure de bibliothèque ne contenait aucun défaut évident, l’équipe pouvait-elle prouver que son implémentation correspondait au comportement arithmétique prévu ?

L’entreprise a construit un exécuteur minimal de Miden VM dans Lean. Lean est un assistant de preuve interactif dont le petit noyau de confiance vérifie qu’une preuve soumise découle de ses définitions et hypothèses. Claude a également aidé à créer un traducteur convertissant des procédures MASM en représentations Lean.

Plusieurs agents ont ensuite travaillé en parallèle sur les preuves de procédures. Le modèle MASM Lean qui en résulte contient une sémantique VM exécutable, des procédures traduites, une infrastructure de preuve partagée et des théorèmes de correction individuels.

Le dépôt répertorie 95 preuves de procédures vérifiées : 31 pour des opérations sur 64 bits, 36 pour des opérations sur 128 bits, 17 pour des opérations sur 256 bits et 11 pour des opérations sur des mots. Ensemble, elles couvrent les parties d’arithmétique binaire décrites par Trail of Bits.

Il ne s’agissait pas de preuves que chaque partie de Miden était sécurisée. Elles portaient sur des propriétés de correction définies pour certaines procédures. Cette limite est essentielle, car un assistant de preuve vérifie le théorème qui lui est fourni, non l’intention non exprimée dans l’esprit d’un développeur.

Trail of Bits indique que les examinateurs humains se sont donc concentrés sur l’audit des énoncés de théorèmes. Si un agent prouvait un théorème omettant une précondition critique ou exprimant le mauvais résultat, l’acceptation par le noyau ne rendrait pas pour autant le logiciel correct.

À haut niveau, de nombreux théorèmes suivaient un schéma reconnaissable. Étant donnée une pile contenant des entrées précises, l’exécution d’une procédure doit se terminer et laisser au sommet le résultat mathématiquement attendu. Les valeurs de pile sans lien, appartenant à l’appelant, doivent rester aux emplacements attendus.

Cette exigence de spécification a révélé deux défauts ignorés par les tests unitaires existants. Le premier affectait une procédure de rotation à droite sur 64 bits nommée rotr. Elle se comportait incorrectement pour de grandes entrées supérieures au nombre premier Goldilocks lorsque la quantité de rotation était un multiple de 32.

Le nombre premier Goldilocks définit le corps utilisé par la VM ; les valeurs proches ou au-delà de cette limite nécessitent donc une représentation soigneuse. Lors du travail de preuve, le théorème souhaité ne pouvait aboutir sans ajouter une hypothèse excluant le cas problématique de décalage.

L’échec d’une preuve ne constitue pas automatiquement la preuve d’un bug de code. Le théorème, le modèle ou les lemmes de soutien peuvent également être erronés. Ici, l’examen manuel de l’obstacle a conduit l’équipe au cas limite de l’implémentation.

Le second bug est apparu dans la procédure wrapping_mul sur 256 bits. Trail of Bits indique qu’elle retirait de la pile des valeurs appartenant à l’appelant avant de retourner. Des tests ordinaires du résultat de multiplication pouvaient réussir tout en omettant de vérifier la préservation de l’état environnant de la pile.

Ce défaut montre pourquoi des postconditions précises importent. Une procédure peut calculer la bonne réponse numérique tout en violant son contrat d’appel. Dans une machine à pile, endommager un état adjacent peut affecter l’exécution ultérieure même lorsque l’élément supérieur semble correct.

Les tests unitaires conservent un rôle central. Ils s’exécutent rapidement, protègent contre les régressions connues et couvrent les comportements d’intégration qui ne disposent peut-être pas encore d’un modèle formel. L’effort Lean a apporté un type d’assurance différent sur des propriétés explicitement énoncées.

L’avantage clé était compositionnel. Les agents pouvaient produire des tentatives de preuve à grande échelle, tandis que le noyau de Lean rejetait les dérivations invalides. Les humains n’avaient pas à faire confiance à l’assurance exprimée en prose par un modèle. Ils devaient examiner les définitions et confirmer que les théorèmes acceptés représentaient les garanties visées.

Il s’agit d’une frontière de contrôle plus robuste que de demander à un autre modèle de langage si du code généré semble correct. Elle n’élimine pas le jugement humain, mais le déplace vers les spécifications et les hypothèses.

Pour les responsables de l’ingénierie, ce cas suggère une répartition pratique du travail. Les agents peuvent générer l’échafaudage répétitif de preuves, des traducteurs et des lemmes candidats. Des spécialistes humains décident de ce qui doit être prouvé et cherchent pourquoi des énoncés importants échouent.

Le résultat ne rend pas les audits autonomes dignes de confiance

Le projet soutient l’ingénierie d’audit assistée par des agents, et non une certification de sécurité sans supervision.

Trail of Bits présente directement le changement économique. Quelques années auparavant, l’entreprise aurait eu du mal à justifier des mois d’outillage exploratoire pour une seule mission. De tels projets annexes avaient des résultats incertains et étaient difficiles à vendre avant que leur valeur ne devienne visible.

L’entreprise affirme que les agents ont suffisamment réduit le coût de l’exploration pour modifier ce calcul. Les expériences échouées coûtent de plus en plus des tokens et du temps de supervision plutôt qu’une mobilisation complète de main-d’œuvre d’ingénierie spécialisée.

Cette affirmation mérite une lecture attentive. Six mois se sont tout de même écoulés avant l’audit, et le seul décompilateur a accumulé plus de 100 commits générés par IA. Le récit public ne fournit pas de comparaison contrôlée entre les heures de personnel, le coût total des modèles ou le rendement en défauts, et une mission conventionnelle.

Il n’établit pas non plus que des agents peuvent construire des outils équivalents pour chaque langage inhabituel. MASM présentait des propriétés favorables à l’analyse et à la modélisation formelle. La Miden VM dispose d’un jeu d’instructions compact, et de nombreuses opérations évitent les effets de bord complexes.

Même dans cette cible favorable, le décompilateur ne pouvait pas couvrir chaque procédure en toute sécurité. Trail of Bits a restreint le sous-ensemble pris en charge, car des effets de pile incohérents et des signatures manquantes rendaient une décompilation complète et fiable impraticable.

Le flux de travail Lean comportait une autre limite. Les preuves vérifiées par le noyau n’établissent que le théorème énoncé selon la sémantique modélisée. Une instruction mal traduite, un modèle VM incomplet ou un théorème faible peut maintenir un écart entre le comportement prouvé et le déploiement réel.

L’examen humain est resté visible tout au long du processus. Les auditeurs ont examiné le code généré par les agents, converti les régressions en tests, inspecté les énoncés de théorèmes et analysé les preuves échouées. Claude et Codex alternaient entre développement et revue plutôt que d’opérer comme une autorité non observée.

Cela rend la comparaison principale plus nette. La revue directe par IA demande à un modèle de reconnaître des vulnérabilités dans une représentation existante. Les agents qui construisent des outils aident les experts à créer une représentation où les contraintes manquantes, les types invalides et les postconditions incorrectes deviennent explicites.

Aucune de ces approches ne devrait être utilisée seule. Les modèles peuvent faire émerger des hypothèses que les analyseurs statiques n’encodent pas. L’analyse statique peut couvrir des chemins d’exécution qu’un examinateur probabiliste pourrait négliger. La preuve formelle peut alors traiter des propriétés sélectionnées selon une norme vérifiable par machine.

Le processus crée également des obligations de maintenance. Les parseurs doivent suivre les évolutions du langage. Les analyseurs ont besoin de suites de régression. Les modèles formels doivent rester alignés sur la sémantique de la VM. Des outils générés qui deviennent obsolètes peuvent créer une fausse assurance.

Trail of Bits rapporte que l’équipe Miden a adopté le moteur d’analyse statique pour les futures mises à jour de la bibliothèque principale. C’est un signal important, car il fait passer l’outillage au-delà d’un instantané d’audit unique. Son utilisation continue testera si l’analyseur reste utile à mesure que le langage et la bibliothèque évoluent.

Les organisations envisageant un flux de travail similaire devraient également prévoir la traçabilité. Les équipes doivent savoir quel modèle a généré une modification, quel humain l’a examinée, quels tests ont été exécutés et quelles hypothèses sont entrées dans une preuve. Un flux de travail d’ingénierie n’est vérifiable que dans la mesure des enregistrements conservés autour de lui.

Les éléments publics soutiennent donc une conclusion circonscrite. Les agents ont rendu un ambitieux programme de préparation réalisable pour cette mission. L’assurance de sécurité provenait toujours du système combiné d’experts du domaine, de tests, d’analyses explicites et de vérification de preuves.

Ce système est plus intéressant que l’affirmation selon laquelle une IA a trouvé un bug. Il propose un modèle concret pour employer des agents imparfaits sans traiter leur assurance comme une preuve.

Trois signaux permettront de déterminer si ce modèle d’audit perdure

Le prochain test consiste à voir si les outils d’assurance construits par des agents restent corrects, adoptés et productifs après les découvertes marquantes.

Le premier signal est l’intégration continue de l’analyseur MASM au processus de développement de Miden. Trail of Bits indique que l’équipe Miden a adopté le moteur d’analyse statique pour les futures modifications de la bibliothèque principale. Son utilisation routinière dans l’intégration continue renforcerait l’argument selon lequel l’outillage d’audit peut devenir une infrastructure préventive.

La mesure importante n’est pas le nombre d’avertissements qu’il émet. Il s’agit de savoir si les nouvelles procédures publiques reçoivent la validation requise avant leur publication, et si les mises à jour de l’analyseur suivent les évolutions de la sémantique MASM. Des faux positifs persistants ou des modèles obsolètes affaibliraient le résultat.

Le deuxième signal est l’extension et la maintenance des 95 preuves Lean. Des procédures vérifiées supplémentaires montreraient que le modèle initial soutient un travail continu plutôt qu’une démonstration figée. Les modifications du code arithmétique existant devraient également déclencher des mises à jour ou des échecs de preuve.

Il faut surveiller la frontière entre le code traduit et les spécifications examinées manuellement. Une automatisation qui augmenterait le nombre de preuves sans renforcer la couverture des théorèmes n’apporterait pas la même assurance. Une documentation claire des hypothèses comptera autant que le total brut.

Le troisième signal est la réplication par d’autres équipes d’audit et écosystèmes de langages. Miden présentait une combinaison particulièrement adaptée : un langage personnalisé, des outils manquants, une sémantique de preuve explicite et des mois de temps de préparation.

Un schéma reproduit sur différents zkVM ou langages de bas niveau soutiendrait l’affirmation économique plus large de Trail of Bits. L’impossibilité de le reproduire sur des systèmes comportant de la concurrence, une mémoire complexe ou de grands graphes de dépendances en révélerait les limites.

L’audit Miden de Trail of Bits a déjà produit davantage qu’un flux de travail spéculatif. Il a livré une intégration d’éditeur, un décompilateur, un analyseur, un modèle VM, des preuves vérifiées et des découvertes de sécurité concrètes.

La question durable est de savoir si les équipes peuvent maintenir ces artefacts alignés sur les systèmes qu’ils protègent. Les développeurs qui évaluent la sécurité assistée par agents devraient examiner les dépôts, inspecter les hypothèses modélisées et se demander où des contrôles vérifiables par machine remplacent la confiance accordée au modèle. C’est le standard à retenir pour le prochain audit.