Le professeur Shao Zhong, co-fondateur de CertiK, a assisté au sommet des chercheurs Web3 et a présenté pour la première fois le modèle LiDO.

Lors de la conférence des chercheurs Web3 2025 qui s’est tenue aujourd’hui, le professeur du département d’informatique de l’Université de Yale et co-fondateur de CertiK, Zhao Zhong, a prononcé un discours intitulé “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. Cette percée vise à fournir une preuve de sécurité et d’activité vérifiable de manière mécanisée 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.

Lors de cette présentation, le professeur Shao Zhong a souligné que les protocoles de consensus existants (comme PBFT, Jolteon), 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 :

• Couche d’abstraction de sécurité : mappe le protocole en une machine à états linéarisée, assurant la cohérence des journaux (sécurité) ;
• Couche de garantie active : introduction du mécanisme “Pacemaker” pour résoudre le problème de latence réseau grâce à la diffusion par timeout et à la synchronisation des tours ;
• Couche d’extension DAG : prend en charge de 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, complétant plus de dix mille lignes de preuves mécaniques de code Coq, avec un volume de code de vérification de sécurité et d’activité atteignant respectivement 4000 lignes et 1700 lignes. “À l’heure actuelle, les protocoles de consensus PoS font face à la difficulté de concilier sécurité, activité et décentralisation,” a souligné le professeur Shao Zhong lors de sa conférence. “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 Zhao Zhong et son équipe, est le premier système d’exploitation “sans vulnérabilité” au monde ayant passé une vérification formelle, et est salué comme un “jalon pour la sécurité des systèmes cyber-physiques”. Cet accomplissement non seulement établit la base technologique de la société de sécurité CertiK, mais met également en lumière son accumulation approfondie dans le domaine de la sécurité des systèmes. Ces dernières années, le professeur Zhao Zhong s’est concentré sur la sécurité de la blockchain, et en 2017, il a co-fondé CertiK avec son disciple, le professeur Gu Ronghui, introduisant la technologie de vérification formelle pour garantir la sécurité des contrats intelligents et des protocoles en chaîne, protégeant ainsi la sécurité 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 a commencé à explorer les possibilités d’intégration avec les principales chaînes publiques et les protocoles décentralisés. Le professeur Shaozhong a déclaré que CertiK s’engage à vérifier les mécanismes clés dans Web3.0 pour fournir des produits et des services sur l’ensemble du cycle, soutenant mieux la stratégie de développement à long terme des entreprises et de l’écosystème Web3. À la fin de son discours, le professeur Shaozhong a souligné : “Une pile de protocoles réseau fiable, sécurisée et vérifiable sera la clé pour accéder à un véritable avenir décentralisé.”