According to PANews 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 safety 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 like Jolteon, completing verification of over ten thousand lines of Coq code. Professor Zhong Shao stated that LiDO addresses the challenge of simultaneously achieving security, liveness, and decentralization in PoS consensus protocols by proposing a systematic solution. Currently, LiDO is exploring collaborations with mainstream public chains to help build a trustworthy decentralized network protocol stack.
