TechFlow rapporte que, le 19 mai, Vitalik Buterin a publié un article sur son blog personnel, dans lequel il indique que la vérification formelle connaît une expansion rapide au sein de l’écosystème de recherche d’Ethereum et, plus largement, dans le domaine du calcul. Cette technique consiste à rédiger des preuves mathématiques vérifiables automatiquement à l’aide d’outils tels que Lean, afin de confirmer la correction du code ; les chercheurs la qualifient de « forme ultime du développement logiciel ». L’article souligne que la vérification formelle s’applique particulièrement bien aux cas où l’objectif est simple mais l’implémentation complexe, notamment pour les signatures résistantes aux ordinateurs quantiques, les STARKs, les algorithmes de consensus et les ZK-EVM — autant de technologies fondamentales d’Ethereum. Vitalik Buterin insiste toutefois sur le fait que la vérification formelle n’est pas infaillible : elle ne parvient pas à capturer intégralement les intentions humaines et comporte des risques tels que des omissions dans les spécifications ou une couverture incomplète de certains fragments de code.
À ce sujet, il exprime une vision optimiste : l’association de l’intelligence artificielle et de la vérification formelle serait complémentaire — l’IA permettrait de générer efficacement de grandes quantités de code, tandis que la vérification formelle en garantirait la justesse. À l’avenir, la sécurité logicielle adopterait une architecture structurée autour d’un « noyau sécurisé » entouré d’un « bac à sable non sécurisé », et Ethereum constituerait l’un des principaux « noyaux sécurisés » de ce modèle.
