Sonic Labs dévoile une bibliothèque de vérification formelle pour les protocoles de consensus DAG

L'équipe derrière la blockchain haute performance de couche 1 Sonic, Laboratoires soniques a introduit une bibliothèque de vérification formelle conçue pour renforcer la sécurité des protocoles de consensus basés sur les DAG. Dirigée par le Dr Bernhard Scholz, directeur de la recherche, cette bibliothèque vise à fournir une preuve mathématique de la sécurité des blockchains à graphes acycliques dirigés (DAG), y compris le réseau compatible EVM de Sonic.

Développée en partenariat avec des chercheurs de l'Université de Sydney et de l'INRIA, cette bibliothèque open source s'appuie sur l'assistant de preuve TLA+. Elle offre un cadre modulaire et réutilisable qui simplifie la modélisation et la vérification des mécanismes de consensus basés sur l'architecture DAG.

La bibliothèque de vérification propose des preuves formelles pour plusieurs protocoles existants basés sur DAG, tels que DAG-Rider, Cordial Miner, Bullshark, Hashgraph et Aleph. Le protocole propriétaire de Sonic a également été vérifié en tant que dérivé dans ce cadre. Cette recherche a été présentée pour la première fois lors de la conférence NASA Formal Methods 2025, qui s'est tenue à Williamsburg, en Virginie, du 11 au 13 juin, et représente une avancée notable dans les normes de vérification de la blockchain.

« Dans la blockchain, les failles de sécurité proviennent souvent d'hypothèses qui ne sont pas vérifiées avant qu'il ne soit trop tard », a déclaré le Dr Bernhard Scholz, directeur de la recherche chez Sonic Labs, dans une déclaration écrite. « Avec cette bibliothèque, nous passons de l'espoir à la preuve, en offrant les outils permettant de vérifier avec une certitude mathématique qu'un protocole se comportera de manière sûre en toutes circonstances. Notre objectif est de rendre la vérification formelle accessible à tous les développeurs de protocoles », a-t-il ajouté.

Alors que la valeur de la blockchain augmente, Sonic Labs lance un cadre de vérification formel pour garantir la sécurité et la fiabilité du protocole

À mesure que la valeur garantie par les réseaux blockchain continue de croître, l'impact potentiel des vulnérabilités des protocoles de consensus devient de plus en plus important, avec des risques tels que la double dépense et des états de registre incohérents. Les tests et audits de code conventionnels sont limités dans leur capacité à garantir des systèmes exempts de bugs. En réponse, une méthode de vérification formelle a été appliquée par Laboratoires soniques , en utilisant des preuves mathématiques pour confirmer la sécurité du protocole dans toutes les conditions possibles.

Cette approche permet non seulement de valider les protocoles de consensus existants, mais aussi d'aider les développeurs à concevoir de nouveaux modèles basés sur des graphes acycliques dirigés ou à adapter les modèles existants. La méthode est actuellement mise en œuvre pour vérifier formellement que la blockchain Sonic ne présente aucun comportement dangereux, en établissant la fiabilité du protocole par une validation mathématique.

En rendant la bibliothèque de vérification accessible au public, l'initiative fournit aux développeurs de blockchain des ressources pour construire des systèmes dont la sécurité est prouvée. Cela devrait améliorer la résilience globale des écosystèmes décentralisés et réduire les besoins en ressources généralement associés à la vérification des protocoles de consensus.