Vitalik publie un article sur la vérification formelle, mettant en avant son rôle dans la sécurité et l’efficacité d’Ethereum

Selon ChainCatcher, Vitalik a publié aujourd’hui un article intitulé « A shallow dive into formal verification », dans lequel il explique comment la vérification formelle peut améliorer à la fois la sécurité et l’efficacité du développement sur Ethereum. Les développeurs peuvent utiliser Lean, le bytecode EVM ou le langage d’assemblage pour écrire du code et en vérifier la correction grâce à des preuves mathématiques automatiquement vérifiables. Vitalik a noté que la vérification formelle convient particulièrement aux systèmes complexes tels que les STARKs, le consensus par tolérance aux fautes byzantines, ZK-EVM et les signatures post-quantiques, même si elle présente des limites, notamment des erreurs de spécification, une couverture incomplète du code et des attaques au niveau matériel.