La proposition met en place des contrats dédiés à la gestion des dépôts et des sorties des constructeurs.
Verity a terminé son travail de vérification en septembre 2026. Les résultats de l’entreprise se sont concentrés sur l’exactitude du bytecode d’exécution de l’EIP, qui est le code de bas niveau qui s’exécuterait réellement en chaîne.
Verity a prouvé trois garanties. Ils confirment que le bytecode gère correctement les scénarios liés aux soumissions des utilisateurs, c’est-à-dire les appels payants, ainsi que les appels SYSTEM. Les appels SYSTEM sont des invocations effectuées par le protocole lui-même plutôt que par un utilisateur ordinaire.
Les preuves, les mutations et les divergences
Verity a utilisé six mutations de bytecode pour confirmer ses propriétés. Un travail de mutation de ce type implique généralement de modifier délibérément le code pour voir si les propriétés indiquées prennent en compte le changement.
Puis sont arrivées les divergences. L’examen de Verity a signalé des problèmes que les chercheurs d’Ethereum doivent résoudre.
Où se situe EIP-8282 dans le processus
La date limite du dernier appel pour l’EIP-8282 était le 1er novembre 2026. Le travail de Verity s’est terminé en septembre, avant cette date limite.
Ce timing donne à la vérification un poids pratique. Les résultats qui arrivent avant la clôture du dernier appel peuvent toujours façonner la spécification.
Ce que cela signifie pour Ethereum
Pour les développeurs et les chercheurs en protocoles, la tâche immédiate est claire. Les divergences signalées par Verity doivent être réconciliées avec la spécification, que ce soit en modifiant le code, en modifiant la spécification ou en clarifiant le comportement prévu.
Les trois garanties donnent aux chercheurs une base plus solide pour ce travail. Ils savent que les chemins d’appel payant et d’appel SYSTÈME se comportent comme spécifié dans les zones prouvées par Verity.
Ce qu’il faudra ensuite surveiller, c’est la façon dont les chercheurs réagissent aux découvertes de Verity. La résolution de ces divergences, et si la spécification finale change en conséquence, montrera l’influence que la vérification formelle a désormais sur le développement du code de base d’Ethereum.
