Le sommet des chercheurs Web3 dévoile pour la première fois le modèle LiDO : fournissant une vérification mécanisée pour des protocoles de consensus complexes

Lors du sommet des chercheurs Web3 de 2025, le professeur Zhao Zhong du département d'informatique de l'université de Yale a donné une conférence intitulée "Preuve de sécurité et d'activité 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. Ce résultat révolutionnaire vise à fournir des preuves de sécurité et d'activité vérifiables mécaniquement pour les protocoles de consensus Byzantine Fault Tolerance (BFT) complexes, posant ainsi une pierre angulaire technique 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, la complexité de leur mise en œuvre cache souvent des vulnérabilités potentielles. Pour résoudre ce problème, le modèle LiDO propose de manière novatrice un cadre de vérification en trois couches :

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

Actuellement, LiDO a été appliqué avec succès au protocole industriel Jolteon (BFT à deux étapes) et à plusieurs protocoles DAG, complétant la preuve mécanique de plus de dix mille lignes de code Coq, avec une quantité de code de vérification de sécurité et de vivacité atteignant respectivement 4000 lignes et 1700 lignes. Le professeur Shao Zhong souligne : "Actuellement, les protocoles de consensus PoS font face à un dilemme où il est difficile d'obtenir à la fois sécurité, vivacité et décentralisation. Le modèle LiDO est justement une solution de conception systématique proposée pour briser ce dilemme."

En tant que principal développeur de CertiKOS, le premier système d'exploitation "sans faille" validé formellement au monde, le professeur Shao Zhong a accumulé une vaste expérience dans le domaine de la sécurité des systèmes. Cet accomplissement a non seulement établi sa position dans le domaine des technologies de sécurité, mais a également mis en évidence les compétences professionnelles de son équipe en matière de sécurité des systèmes. Ces dernières années, le professeur Shao Zhong a tourné son attention vers la sécurité des blockchains et, en 2017, a cofondé une entreprise axée sur la sécurité des blockchains avec des partenaires, introduisant des techniques de validation formelle dans la protection de la sécurité des contrats intelligents et des protocoles en chaîne, offrant une protection de sécurité pour des actifs cryptographiques évalués à des centaines de milliards de dollars.

Le modèle LiDO a actuellement terminé sa conception et sa vérification formelle, et commence à explorer les possibilités d'intégration avec les principales chaînes publiques et les protocoles décentralisés. Le professeur Shao Zhong a déclaré qu'ils s'engagent à vérifier les mécanismes clés dans Web3.0, afin de fournir des produits et des services sur l'ensemble du cycle, et de mieux soutenir les stratégies 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 fiable, sécurisée et vérifiable sera le chemin clé vers un véritable avenir décentralisé."