Au sommet des chercheurs Web3, le professeur de Yale dévoile pour la première fois le modèle LiDO.

Lors du sommet des chercheurs Web3 de 2025 qui s'est tenu récemment, le professeur Shao Zhong du département d'informatique de l'Université de Yale a prononcé un discours intitulé « Preuve de sécurité et d'activité des protocoles de consensus affinés : LiDO et son extension ». Il a révélé pour la première fois le modèle LiDO développé par son équipe et le cadre d'extension LiDO-DAG. Cette innovation vise à fournir des preuves de sécurité et d'activité vérifiables mécaniquement pour des protocoles de consensus tolérants aux pannes byzantines (BFT) complexes, établissant ainsi une base technologique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.

Le professeur Shao Zhong a souligné dans son discours que, bien que les protocoles de consensus existants (comme PBFT, Jolteon) soient largement utilisés, leur complexité de mise en œuvre cache souvent des vulnérabilités potentielles. Pour résoudre ce problème, le modèle LiDO propose de manière innovante un cadre de vérification en trois couches :

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

Actuellement, LiDO a été appliqué avec succès au protocole industriel Jolteon (BFT à deux étapes) et à plusieurs protocoles DAG, et a complété plus de 10 000 lignes de code Coq pour des preuves mécaniques, dont la quantité de code pour la vérification de la sécurité et de l'activité atteint respectivement 4 000 lignes et 1 700 lignes. Le professeur Shao Zhong a souligné dans son discours : "Actuellement, les protocoles de consensus PoS font face à des défis difficiles à concilier en matière de sécurité, d'activité et de décentralisation. Le modèle LiDO a été proposé comme une solution systémique pour surmonter cette impasse."

L'équipe dirigée par le professeur Zhao Zhong a développé CertiKOS, le premier système d'exploitation "sans faille" au monde validé formellement, salué comme un "jalon de la sécurité des systèmes cyber-physiques". Cet accomplissement a non seulement établi leur solide fondation dans le domaine de la sécurité des systèmes, mais a également démontré leur riche expérience dans ce domaine. Ces dernières années, le professeur Zhao Zhong s'est concentré sur la recherche en sécurité blockchain et a cofondé en 2017 une entreprise de sécurité avec des collègues, introduisant la technologie de validation formelle dans la protection de la sécurité des contrats intelligents et des protocoles on-chain, offrant une protection sécuritaire pour des actifs cryptographiques d'une valeur de plusieurs milliards de dollars.

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