Actualités Foresight, message tiré d’un billet sur le forum d’Ethresearch : des équipes de recherche de l’Ethereum Protocol Fellowship (EPF) et d’Invisible Garden ont annoncé les derniers progrès du projet Etheorem. L’objectif est de construire, à l’aide du langage de preuve par théorèmes Lean 4, un ensemble entièrement exécutable de spécifications de consensus pour Ethereum. La démarche consiste à remplacer les tests de code classiques par des validations formelles mathématiques strictes, afin d’identifier dès la racine les vulnérabilités logiques et d’éviter des incidents de fork de chaîne causés par des écarts de compréhension lors de l’implémentation des spécifications par plusieurs clients. À ce stade, cette spécification a déjà passé l’ensemble des vecteurs de test des trois versions de hard fork futures : Fulu, Gloas (incluant le mécanisme ePBS) et Heze. Elle couvre des éléments essentiels comme la transition d’état et la sélection lors des forks. Toute la logique est vérifiée mathématiquement de manière indépendante par le noyau Lean. Le projet est en train d’établir un cadre de validation de base visant à définir des standards de sécurité élevés pour les futures mises à niveau complexes d’Ethereum.