Buterin affirme que la vérification formelle par IA renforce la sécurité des cryptomonnaies

Buterin publie un nouvel article sur l'IA et la sécurité du code

Le co-fondateur d'Ethereum Vitalik Buterin a publié un article de blog le 18 mai 2026 sur vitalik.eth.limo. Dans cet article, il soutient que la vérification formelle assistée par IA deviendra l'un des outils les plus importants de la cybersécurité. La vérification formelle est une méthode qui utilise des preuves mathématiques pour confirmer que le logiciel se comporte exactement comme prévu. Buterin déclare que la combinaison de l'IA avec la vérification formelle aidera les développeurs à trouver des vulnérabilités avant que les attaquants ne le fassent.

Claude Mythos nommé comme exemple de la puissance de l'IA

Buterin cite Claude Mythos, un modèle d'IA développé par Anthropic, comme un exemple de systèmes d'IA de plus en plus puissants. Il soutient que de tels systèmes peuvent accélérer la découverte et l'exploitation des vulnérabilités. Claude Mythos est un modèle réel. Anthropic a confirmé son existence après une fuite de données accidentelle en mars 2026. Un aperçu du modèle a été publié à des partenaires sélectionnés en avril 2026.

Buterin énumère les limites de la vérification formelle

Buterin souligne que la vérification formelle n'élimine pas tous les risques. Les systèmes de preuve peuvent manquer des hypothèses critiques ou ne pas couvrir les vulnérabilités matérielles et les surfaces d'attaque adjacentes. Il avertit également que l'IA abaisse la barrière à la génération de grands volumes de logiciels. Cela augmente le risque que du code non sécurisé ou mal compris entre dans les systèmes de production. Malgré ces limites, Buterin soutient que l'approche réduit le risque catastrophique par rapport au développement logiciel traditionnel.

Le projet Arklib vise une implémentation STARK vérifiée

Buterin met en avant Arklib comme un exemple concret de méthodes formelles appliquées à Ethereum. Arklib est un projet open-source qui vise à construire une implémentation entièrement vérifiée formellement d'un système de preuve STARK. Un STARK est un type de preuve cryptographique utilisé dans l'infrastructure de mise à l'échelle d'Ethereum. La Fondation Ethereum a financé Nethermind pour étendre Arklib avec la formalisation du protocole FRI dans l'assistant de preuve Lean. Buterin fait également référence à des implémentations vérifiées formellement de la machine virtuelle Ethereum écrites directement en assembleur RISC-V.