Vérification formelle ? Qu'est-ce que c'est ? En savoir plus 🧵
Des trillions de dollars sont stockés dans des blockchains. Un bug de consensus = vidage instantané. Les tests peuvent trouver des bugs mais ne peuvent pas prouver qu'ils sont impossibles. La vérification formelle pour les protocoles basés sur les DAG change la donne.
La vérification formelle modélise un protocole comme une machine d'état et permet à un prouveur de vérifier de manière exhaustive chaque transition, et pas seulement un échantillon de test.
La partie difficile ? Les preuves sont lentes à rédiger. L'idée de Sonic : décomposer les protocoles en blocs de construction réutilisables au lieu de réinventer les preuves à chaque fois.
Sonic Labs vient de rendre open source une bibliothèque TLA+ qui prouve mathématiquement la sécurité pour DAG-Rider, Hashgraph, Bullshark, Aleph et plus encore—sans paywall, sans NDA.
Dijkstra : « Les tests de programme peuvent montrer la présence de bogues, mais jamais leur absence. » Les preuves vous donnent la partie absence.
La bibliothèque divise les choses en deux :
• Construction de DAG 🌳
• Ordonnancement / élection de leader 🗳️
Chaque bloc a sa propre spécification + preuve vérifiée par machine.
Il a fallu environ 14 mois-personnes répartis sur 5 chercheurs pour modéliser 5 protocoles. Ajouter un 6ème prend maintenant des jours, pas des mois.
Le travail a été présenté au NASA Formal Methods 2025. S'il est suffisamment robuste pour les fusées, il est probablement bon pour Sonic !
Avertissement : ces preuves couvrent la sécurité (pas de forks, pas de doubles dépenses). Elles ne corrigent pas la vivacité ou les attaques économiques, mais éliminer complètement des classes entières de bugs de sécurité est tout de même une grande victoire.
TL;DR — Les listes de contrôle d'audit sont de 2020. Les preuves composables et open-source sont de 2025. Faisons de "prouvablement sûr" la norme dans la crypto.
Blog →
Code →
4,84 k
35
Le contenu de cette page est fourni par des tiers. Sauf indication contraire, OKX n’est pas l’auteur du ou des articles cités et ne revendique aucun droit d’auteur sur le contenu. Le contenu est fourni à titre d’information uniquement et ne représente pas les opinions d’OKX. Il ne s’agit pas d’une approbation de quelque nature que ce soit et ne doit pas être considéré comme un conseil en investissement ou une sollicitation d’achat ou de vente d’actifs numériques. Dans la mesure où l’IA générative est utilisée pour fournir des résumés ou d’autres informations, ce contenu généré par IA peut être inexact ou incohérent. Veuillez lire l’article associé pour obtenir davantage de détails et d’informations. OKX n’est pas responsable du contenu hébergé sur des sites tiers. La détention d’actifs numériques, y compris les stablecoins et les NFT, implique un niveau de risque élevé et leur valeur peut considérablement fluctuer. Examinez soigneusement votre situation financière pour déterminer si le trading ou la détention d’actifs numériques vous convient.