On April 8th, at the 2025 Web3 Scholars Summit, Professor Zhong Shao, Director of the Computer Science Department at Yale University and Co-founder of CertiK, publicly unveiled the LiDO model and LiDO-DAG extension framework for the first time. This breakthrough achievement provides mechanically verifiable security and liveness proofs for complex Byzantine Fault Tolerant (BFT) consensus protocols through a three-layer refined verification framework (security abstraction layer, liveness guarantee layer, DAG extension layer), aiming to enhance the reliability and scalable development of the Web3 ecosystem.
LiDO has been successfully applied to industrial-grade protocols such as Jolteon, completing verification of over ten thousand lines of Coq code. Professor Shao stated that LiDO offers a systematic solution to the challenge of simultaneously achieving security, liveness, and decentralization in PoS consensus protocols. Currently, LiDO is exploring collaborations with mainstream public chains to help build a trustworthy decentralized network protocol stack.
