According to PANews, at the 2025 Web3 Scholars Summit, Professor Zhong Shao, Chair of the Computer Science Department at Yale University and co-founder of CertiK, introduced the LiDO model and its LiDO-DAG extension framework. This groundbreaking development offers a mechanized verification of security and liveness proofs for complex Byzantine Fault Tolerance (BFT) consensus protocols through a three-layer refined verification framework, which includes a security abstraction layer, a liveness assurance layer, and a DAG extension layer. The aim is to enhance the reliability and scalability of the Web3 ecosystem.
LiDO has already been successfully applied to industrial-grade protocols like Jolteon, completing verification of over ten thousand lines of Coq code. Professor Shao stated that LiDO provides a systematic solution to the challenges of balancing security, liveness, and decentralization in Proof of Stake (PoS) consensus protocols. Currently, LiDO is exploring collaborations with major public blockchains to help build a trustworthy decentralized network protocol stack.
Alex
