Au sommet des universitaires Web3, un professeur de Yale présente pour la première fois le modèle LiDO.

Lors du sommet des chercheurs Web3 de 2025, le professeur Zhao Zhong du département d'informatique de l'université de Yale a donné un discours principal intitulé "Preuve de sécurité et de vivacité des protocoles de consensus affinés : LiDO et son cadre d'extension". Il a présenté pour la première fois le modèle LiDO développé par son équipe et le cadre d'extension LiDO-DAG. Cette avancée révolutionnaire vise à fournir des preuves de sécurité et de vivacité vérifiables de manière mécanique pour des protocoles de consensus tolérants aux pannes byzantines (BFT) complexes, établissant ainsi une base technique pour la fiabilité et le développement à grande échelle de l'écosystème Web3.

Le professeur Shao Zhong a souligné que les protocoles de consensus existants, bien qu'ils soient largement utilisés, cachent souvent des vulnérabilités potentielles en raison de leur complexité de mise en œuvre. 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 une machine d'état linéarisée pour garantir la cohérence des journaux (sécurité) ;
2. Couche de garantie active : introduction du mécanisme "Pacemaker" pour résoudre le problème des retards réseau grâce à la diffusion par timeout et à la synchronisation des tours ;
3. Couche d'extension DAG : support des nouveaux protocoles DAG, permettant 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, ayant complété plus de 10 000 lignes de code Coq pour la preuve mécanisée, avec un volume de code pour la vérification de la sécurité et de l'activité atteignant respectivement 4000 et 1700 lignes. Le professeur Shao Zhong a souligné lors de sa présentation : "Actuellement, les protocoles de consensus PoS font face à la difficulté d'atteindre simultanément la sécurité, l'activité et la décentralisation. Le modèle LiDO est précisément une solution de conception systématique proposée pour briser cette impasse."

Le CertiKOS, développé par le professeur Shao Zhong et son équipe, est le premier système d'exploitation "sans vulnérabilité" au monde ayant réussi une vérification formelle, et est considéré comme "un jalon pour la sécurité des systèmes cyber-physiques". Cet accomplissement non seulement établit sa base technique dans le domaine de la sécurité des systèmes, mais met également en évidence son accumulation profonde. Ces dernières années, le professeur Shao Zhong s'est concentré sur la sécurité de la blockchain, et en 2017, il a introduit avec son disciple, le professeur Gu Ronghui, la technologie de vérification formelle dans la protection de la sécurité des contrats intelligents et des protocoles sur chaîne, garantissant la sécurité d'actifs cryptographiques évalués à des milliards de dollars.

LiDO a actuellement terminé la conception du modèle et la validation formelle, et commence à explorer la possibilité d'intégration avec des chaînes de blocs grand public et des protocoles décentralisés. Le professeur Zhao Zhong a déclaré qu'ils s'efforcent de valider les mécanismes clés du Web3.0 afin de fournir des produits et services sur l'ensemble du cycle, soutenant ainsi mieux les stratégies de développement à long terme des entreprises et de l'écosystème Web3. À la fin de son discours, le professeur Zhao Zhong a souligné : "Une pile de protocoles réseau fiable, sécurisée et vérifiable sera la clé du chemin vers un véritable avenir décentralisé."