Le cofondateur d’Ethereum, Vitalik Buterin, a publié le 18 mai une analyse approfondie portant sur l’état actuel et les perspectives des techniques de vérification formelle (Formal Verification). Il estime que la vérification formelle assistée par l’IA deviendra « la forme ultime du développement logiciel », et indique qu’Ethereum jouera un rôle important dans l’architecture de « cœur de sécurité » du futur.
Principes fondamentaux de la vérification formelle et cas d’usage
D’après l’article de Vitalik, la vérification formelle s’avère particulièrement adaptée aux scénarios où « l’objectif est bien plus difficile que la mise en œuvre ». Il liste clairement quatre composants technologiques clés pour la prochaine étape de mise à niveau d’Ethereum :
Signatures résistantes aux attaques quantiques : travaux de vérification formelle déjà réalisés sur des variantes de signatures SPHINCS
Systèmes de preuves STARK : le projet Arklib vise à créer une implémentation STARK entièrement vérifiée formellement
Algorithmes de consensus tolérant aux fautes byzantines : efforts actuels pour formaliser et prouver les propriétés de sécurité du consensus Lean
ZK-EVM : le projet evm-asm vise à établir une implémentation d’EVM intégralement vérifiée formellement (écriture en assembleur RISC-V)
Vitalik cite l’idée de Yoichi Hirai, et qualifie cette approche de « forme ultime du développement logiciel ».
Orientation de l’évolution de l’architecture « cœur de sécurité » décrite par Vitalik
D’après l’article de Vitalik, il décrit le schéma d’évolution futur de l’architecture logicielle :
Cœur de sécurité : renforcement continu par des méthodes formelles, porteur de la confiance la plus élevée ; Vitalik indique explicitement qu’Ethereum, le noyau des systèmes d’exploitation et les applications liées à l’Internet des objets deviendront le cœur de sécurité.
Périphérie non sûre : les composants périphériques s’exécutent dans un environnement sandbox, avec les autorisations minimales nécessaires à l’accomplissement des tâches ; si un composant périphérique tombe en panne, le cœur de sécurité assure la protection.
Limites de confirmation et modes d’échec de la vérification formelle
Vitalik reconnaît que la vérification formelle n’est pas une solution miracle. Il s’appuie sur les travaux de chercheurs comme Nadim Kobeissi (Cryspen) pour confirmer trois principaux modes d’échec : omission partielle de la vérification (seule une partie du code est vérifiée, tandis que les parties non vérifiées présentent des défauts critiques) ; oubli dans les spécifications (erreurs dans le document de sécurité lui-même ou hypothèses erronées incluses dans la preuve) ; attaques par canal auxiliaire (attaques par canaux latéraux à la frontière entre logiciels et matériels difficiles à capturer avec les modèles existants).
Vitalik souligne que « l’exactitude prouvable » vérifie, par essence, la cohérence interne entre différentes intentions exprimées, plutôt que la correspondance absolue avec les intentions réelles des êtres humains.
Outils de vérification formelle assistée par l’IA
D’après l’article de Vitalik, les outils disponibles comprennent : Lean (langage de preuve mathématique permettant de vérifier automatiquement des théorèmes) ; Claude et Deepseek 4 Pro (Vitalik confirme qu’ils sont suffisants pour écrire des preuves Lean) ; Leanstral (modèle à poids ouvert de 1190 milliards de paramètres, spécialisé dans un fine-tuning pour l’écriture de Lean, exécutable localement, et affichant de meilleures performances aux tests de référence que de nombreux modèles généralistes plus grands).
FAQ
Pourquoi Vitalik pense-t-il qu’Ethereum doit devenir un « cœur de sécurité » ?
D’après l’article de Vitalik, Ethereum est similaire au noyau d’un système d’exploitation : il porte le plus haut niveau de confiance dans le processus de numérisation de la société. Il indique que l’objectif de conception du cœur de sécurité est d’atteindre une norme de sécurité qui n’autorise pas la prolifération de codes défectueux, et de consacrer toute la puissance de calcul additionnelle apportée par l’IA à l’amélioration de la sécurité du cœur de sécurité.
Pourquoi la vérification formelle convient-elle particulièrement à des technologies comme STARK, ZK-EVM, etc. ?
D’après l’analyse de Vitalik, leur point commun est que « l’objectif est bien plus difficile que la mise en œuvre » : leurs propriétés de sécurité peuvent être définies clairement via un langage mathématique, mais l’implémentation concrète est extrêmement complexe, ce qui correspond précisément au terrain où la vérification formelle est la plus utile.
Comment Vitalik conseille-t-il aux développeurs d’utiliser concrètement la vérification formelle assistée par l’IA ?
D’après l’article de Vitalik, il recommande de laisser l’IA écrire le code Lean et les preuves mathématiques ; dans le final, l’utilisateur doit seulement vérifier que les énoncés prouvés correspondent à l’attendu, sans avoir à écrire lui-même le pénible code de preuve de bas niveau. Il confirme que Claude, Deepseek 4 Pro et Leanstral sont les principaux outils disponibles à l’heure actuelle.
Avertissement : Les informations figurant sur cette page peuvent provenir de sources tierces et sont fournies à titre indicatif uniquement. Elles ne reflètent pas les points de vue ou opinions de Gate et ne constituent pas un conseil financier, d’investissement ou juridique. Le trading des actifs virtuels comporte des risques élevés. Veuillez ne pas vous fonder uniquement sur les informations de cette page pour prendre vos décisions. Pour en savoir plus, consultez l’
avertissement.
