Ethereum : Vitalik Buterin veut sécuriser le code avec l'IA et les maths

L'IA au service de la sécurité d'Ethereum

Vitalik Buterin, cofondateur d'Ethereum, a publié une analyse détaillée sur la sécurisation du code blockchain. Sa proposition repose sur deux piliers : l'intelligence artificielle et la vérification formelle.

C'est quoi la vérification formelle ?

Concrètement, il s'agit de traiter un programme informatique comme un objet mathématique. L'objectif : prouver rigoureusement qu'un code se comporte exactement comme prévu, sans surprise ni faille cachée.

Des outils spécialisés comme Lean permettent de réaliser ces démonstrations mathématiques. Jusqu'ici, leur complexité les réservait à une poignée d'experts.

Pourquoi l'IA change la donne

Selon Buterin, les progrès récents de l'IA rendent ces méthodes bien plus accessibles aux développeurs ordinaires. L'IA peut aider à rédiger et vérifier ces preuves mathématiques, réduisant considérablement le temps et les compétences nécessaires.

Des applications concrètes sur Ethereum

Buterin cible en priorité les infrastructures critiques du réseau :

• Les ZK proofs (preuves à divulgation nulle de connaissance), essentielles à la confidentialité et à la scalabilité
• Les signatures post-quantiques, conçues pour résister aux futurs ordinateurs quantiques

Cette démarche s'inscrit dans un contexte de montée des cyberattaques assistées par IA, qui rendent les vulnérabilités logicielles encore plus dangereuses.

Buterin précise toutefois que la vérification formelle ne garantit pas une sécurité absolue : elle prouve qu'un code respecte ses spécifications, mais ces spécifications doivent elles-mêmes être correctement définies.