Vitalik Buterin a souligné la vérification formelle comme une avancée cruciale pour le développement logiciel d'Ethereum. Cette méthode consiste à utiliser des langages comme Lean pour créer des preuves mathématiques pouvant être automatiquement vérifiées, renforçant ainsi la sécurité des technologies complexes telles que les protocoles de communication chiffrée, les ZK-STARKs et les algorithmes de consensus. L'intégration de l'IA a encore simplifié ce processus, permettant la génération automatique de preuves de vérification et de code assembleur. Buterin insiste sur le fait que la valeur fondamentale de la vérification formelle réside dans sa capacité à séparer le code central sécurisé des composants moins sûrs, permettant aux utilisateurs de vérifier les preuves de sécurité sans avoir à examiner l'ensemble du code. Cependant, il met en garde que la vérification formelle n'est pas une solution miracle, car elle ne peut garantir l'alignement avec l'intention humaine et a connu des échecs de vérification. Malgré ces défis, la vérification formelle offre une voie prometteuse pour renforcer la sécurité du réseau face à la montée du code généré par l'IA.