Le modèle LiDO présenté pour la première fois au sommet des chercheurs Web3, offrant une nouvelle perspective sur la sécurité des protocoles de consensus.

Lors du récent sommet des chercheurs Web3 2025, un professeur du département d'informatique de l'université de Yale a prononcé un discours principal intitulé « La sécurité et la preuve d'activité des protocoles de consensus raffinés : LiDO et son cadre d'extension ». C'était la première fois qu'il présentait au public le modèle LiDO développé par son équipe ainsi que le cadre d'extension LiDO-DAG. Ce résultat innovant vise à fournir des preuves de sécurité et d'activité vérifiables mécaniquement pour des protocoles de consensus Byzantine Fault Tolerance (BFT) complexes, posant ainsi une base technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.

Le professeur a souligné dans son discours que, bien que les protocoles de consensus existants (comme PBFT, Jolteon) soient largement utilisés, leur complexité d'implémentation cache souvent des vulnérabilités de sécurité potentielles. Pour résoudre ce problème, le modèle LiDO propose de manière innovante un cadre de validation à trois niveaux :

1. Couche d'abstraction de sécurité : mappe le protocole en une machine d'état linéarisée, garantissant la cohérence des journaux (sécurité) ;
2. Couche de garantie d'activité : introduction du mécanisme "Pacemaker", qui résout les problèmes de latence réseau par la diffusion d'un dépassement de délai et la synchronisation des tours ;
3. Couche d'extension DAG : prend en charge les nouveaux protocoles DAG émergents tels que Narwhal et Bullshark, permettant une validation efficace du consensus sans leader.

Actuellement, LiDO a été appliqué avec succès au protocole industriel Jolteon (BFT à deux étapes) et à plusieurs protocoles DAG, ayant réalisé plus de dix mille lignes de preuves mécaniques de code Coq, où les lignes de code pour la vérification de la sécurité et de l'activité ont respectivement atteint 4000 et 1700 lignes. Ce professeur a souligné lors de sa présentation : "Actuellement, les protocoles de consensus PoS font face à la difficulté d'obtenir simultanément la sécurité, l'activité et la décentralisation. Le modèle LiDO est en effet une proposition de conception systématique visant à surmonter ce goulet d'étranglement."

Il convient de mentionner que ce professeur a précédemment dirigé une équipe qui a développé le tout premier système d'exploitation « sans faille » CertiKOS grâce à la vérification formelle, salué par l'industrie comme un « jalon pour la sécurité des systèmes cyber-physiques ». Cet accomplissement a non seulement jeté les bases techniques pour la société de sécurité qu'il a fondée par la suite, mais il démontre également son expertise approfondie dans le domaine de la sécurité des systèmes. Ces dernières années, ce professeur a approfondi ses recherches sur la sécurité blockchain, intégrant la technologie de vérification formelle dans le domaine de la sécurité des contrats intelligents et des protocoles en chaîne, fournissant une protection sécuritaire pour des actifs cryptographiques d'une valeur de plusieurs centaines de milliards de dollars.

Le modèle LiDO a actuellement terminé la conception et la vérification formelle, et commence à explorer les possibilités d'intégration avec les principales blockchains et les protocoles décentralisés. Ce professeur a déclaré qu'ils s'engagent à vérifier les mécanismes clés dans Web3.0 pour fournir des produits et des services sur l'ensemble du cycle, afin de mieux soutenir la stratégie de développement à long terme des entreprises et des écosystèmes Web3. À la fin de son discours, il a souligné : "Une pile de protocoles réseau fiable, sécurisée et vérifiable sera le chemin clé vers un avenir véritablement décentralisé."