Vitalik : La vérification formelle assistée par l'IA pourrait améliorer à la fois l'efficacité et la sécurité du code.

Foresight News rapporte que Vitalik Buterin a publié un article explorant les perspectives d'application de la vérification formelle dans le domaine de la sécurité blockchain. L'article souligne qu'une nouvelle approche émerge dans la recherche avancée sur Ethereum : elle consiste à écrire directement le code en EVM bytecode, en assembleur ou en Lean, puis à vérifier sa validité à l'aide de preuves mathématiques pouvant être vérifiées automatiquement dans Lean. Le chercheur Yoichi Hirai qualifie cette approche de « forme ultime du développement logiciel ». Vitalik estime que la vérification formelle assistée par intelligence artificielle promet d’améliorer à la fois l’efficacité et la sécurité du code, en particulier pour les modules critiques de sécurité tels que STARK, ZK-EVM, les signatures résistantes aux ordinateurs quantiques et les algorithmes de consensus. L’article souligne également que la vérification formelle n’est pas une solution universelle, puisqu’elle peut échouer en raison de la portée incomplète des preuves, d’erreurs de spécification ou de failles matérielles. À l’avenir, les logiciels pourraient se scinder entre des « noyaux de sécurité » et des « périphéries non sécurisées », Ethereum étant appelé à devenir l’un des principaux noyaux de sécurité.