Le bug @Zcash a conduit à Ironwood, la vérification formelle du circuit de paiement Orchard. J'aime et soutiens ce projet. Je tiens également à souligner que @Starknet effectue ce type de vérification formelle depuis plus de cinq ans. Il est important de soutenir de grands projets comme Zcash pour leur réactivité rapide, comme dans ce cas. Il est également essentiel de reconnaître les projets qui sont futuristes et en avance sur leur temps, comme Starknet. (Détails dans l’article ci-dessous) J’ai souvent dit que Starknet est le système qui possède déjà les fonctionnalités que d’autres chaînes prétendent déployer prochainement. Cela a été vrai pour de nombreux aspects. Nous avons été à l’avant-garde de plusieurs choix impopulaires que tout le monde reconnaît aujourd’hui comme essentiels, notamment les ZK-STARKs résistants à l’ordinateur quantique comme meilleure solution pour le scaling et la confidentialité, les zkVM légers (Cairo est le meilleur), la disponibilité des données Validium et la vérification formelle. La vérification formelle signifie que vous utilisez des outils automatisés comme le système Lean pour prouver mathématiquement que votre code est sûr. Il est très difficile de capturer chaque aspect de ce que signifie pour un code d’être sûr, mais sous la direction de notre CTO @LiorGoldberg2 (co-créateur du zkVM et du langage Cairo), nous y travaillons depuis plus de cinq ans. Le tout premier article sur la vérification formelle de revendications liées aux ZK (Professeur Jeremy Avigad, Yoav Seginer, et d’autres) a démontré que l’ensemble des contraintes polynomiales définissant le VM Cairo est correct. Si vous avez suivi l’actualité récemment, le bug récemment découvert par l’IA et désormais corrigé pour Zcash (un autre projet que j’ai cofondé, dont je suis très fier et que je soutiens) concernait une contrainte manquante. La décision de vérifier leur code afin d’éliminer d’autres tels bugs est la bonne démarche. L’exécution de ce type de vérification pour le VM central Cairo nous a fourni, à l’équipe StarkWare, une certitude mathématique qu’il n’existe aucune contrainte manquante dans notre VM Cairo. Ainsi, en plus de prouver le VM central de Cairo, nous avons également prouvé le système S-two STARK, partie du compilateur, et de nombreuses fonctions de la bibliothèque standard Cairo. Le travail est-il terminé ? Non. Il existe de nombreux autres éléments qui peuvent être prouvés formellement. Mais nous nous engageons à continuer à prouver formellement toutes les propriétés fondamentales liées à la solidité et à la sécurité de nos systèmes. Il est excellent de voir d’autres projets adopter la vérification formelle comme outil essentiel. Je suis fier que StarkWare ait également ouvert la voie dans ce domaine. C’est ce que signifie pour nous une blockchain futuriste. Envie d’en savoir plus ? Voici un compte rendu détaillé de nos efforts de preuve avec Lean au cours des dernières années