Le co-fondateur d'Ethereum, Vitalik Buterin, a proposé un nouveau langage de programmation. Il se compilerait directement en Lean ou HOL, un autre assistant de preuve formelle.
L'idée cible un écart spécifique dans la façon dont les gens lisent les résultats de l'IA. L'intelligence artificielle produit de plus en plus de grands blocs de preuves automatisées, souvent plus rapidement que n'importe quelle équipe humaine ne pourrait les écrire à la main. Peu de lecteurs peuvent rapidement confirmer ce que ces preuves établissent réellement.
Un langage construit uniquement pour les lecteurs de preuves IA
Lean est un assistant de preuve, un logiciel que les mathématiciens et les ingénieurs utilisent pour écrire des preuves qu'un ordinateur peut vérifier ligne par ligne. Les chercheurs d'Ethereum l'utilisent déjà pour vérifier le code cryptographique et la logique de consensus. Les assistants de preuve existent depuis près de 60 ans, mais le domaine est resté une poursuite de niche.
Dans son post, Buterin a soutenu que les étapes internes d'une preuve n'ont qu'une seule exigence. Cette exigence est la correction mathématique, rien de plus. Les lecteurs n'inspectent jamais cette machinerie directement. Les définitions et les théorèmes fonctionnent différemment, car les humains lisent ces parties pour apprendre ce que garantit réellement un morceau de logiciel.
Buterin a exploré une division connexe dans un post de blog de mai. Là, une preuve mathématique montre qu'un code bas niveau efficace correspond à une spécification lisible séparée, de sorte qu'un seul audit couvre les deux versions à la fois.
Son timing coïncide également avec l'effort de reconstruction d'Ethereum, qui porte un surnom distinct, la feuille de route Lean Ethereum. Pendant ce temps, les chercheurs construisent un ZK-EVM formellement vérifié, une version de la machine virtuelle d'Ethereum (EVM) prouvable par zéro connaissance, en utilisant des méthodes comparables.
L'IA écrit les preuves, les humains vérifient les affirmations
Les grands modèles de langage peuvent déjà écrire des preuves Lean utilisables. Buterin a nommé Claude et Deepseek 4 Pro comme outils capables, aux côtés de Leanstral, un modèle plus petit spécifiquement ajusté pour Lean. Un projet exemple est evm-asm, une implémentation EVM vérifiée contre une référence lisible. Cette capacité fait écho aux compétences de raisonnement que les développeurs ont affichées lors d'un récent défi AI de Buterin. Les testeurs ont résolu ce défi en quelques heures.
Les enjeux vont au-delà de la commodité, cependant. Les chercheurs en sécurité ont suivi une augmentation des tentatives d'exploitation assistées par l'IA cette année. Le code formellement vérifié offre une défense contre cette tendance. Un langage de spécification plus convivial permettrait aux développeurs d'auditer les affirmations sans avoir à se plonger dans la preuve environnante.
Au-delà des cercles de recherche d'Ethereum
Buterin continue de tester ces idées en public, comme il l'a récemment démontré avec un panneau d'affichage anonyme construit avec des preuves à zéro connaissance. La démonstration a montré comment des affirmations vérifiables peuvent passer des dépôts de recherche à des produits fonctionnels. Les chercheurs ont également commencé à vérifier formellement les clients de consensus dans Lean pour détecter les bogues tôt.
Pourtant, la direction fait écho à un schéma familier : séparer le code rapide des revendications lisibles, puis prouver que les deux correspondent.
Aucun prototype du nouveau langage n'existe encore, et Buterin a laissé la syntaxe exacte ouverte. Les développeurs peuvent converger vers un standard commun, ou opter pour plusieurs dialectes incompatibles à la place. Ce choix pourrait déterminer la rapidité avec laquelle le code vérifié par l'IA atteint les systèmes de production.
Source : BeInCrypto
