TechFlow annonce que, le 18 mai, Vitalik a publié un article intitulé « A shallow dive into formal verification », présentant les avancées récentes de la vérification formelle dans la recherche et le développement de pointe d’Ethereum. Selon cet article, les développeurs peuvent écrire du code en utilisant des langages tels que Lean, le bytecode EVM ou l’assembleur, puis prouver mathématiquement sa correction à l’aide de preuves vérifiables automatiquement, ce qui améliore simultanément l’efficacité et la sécurité du code.
Il précise que la vérification formelle s’applique particulièrement bien à des systèmes complexes mais dont les objectifs de sécurité sont relativement clairs, tels que les STARK, les protocoles de consensus tolérants aux pannes byzantines (BFT), les ZK-EVM et les signatures résistantes aux ordinateurs quantiques. Il cite notamment des projets connexes tels qu’Arklib, VCV-io et evm-asm. L’article souligne toutefois que la vérification formelle n’est pas une solution universelle : elle peut encore être limitée par des erreurs dans la spécification, des parties de code non couvertes par la vérification, les contraintes matérielles ou les attaques par canaux auxiliaires.
