The Web3 Scholars Summit Focuses on the Security of Consensus Protocols and Proof of Activity

At the recently held 2025 Web3 Scholars Summit, a well-known computer science professor delivered a keynote speech titled "Refined Consensus Protocol Security and Liveness Proof: LiDO and Its Extensions," where he publicly unveiled the LiDO model and the LiDO-DAG extension framework developed by his team for the first time. This groundbreaking achievement aims to provide mechanizable verification of security and liveness proof for complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a technological foundation for the reliability and scalable development of the Web3 ecosystem.

The speaker pointed out that existing consensus protocols (such as PBFT, Jolteon) are widely used, but their complex implementation often hides potential vulnerabilities. To address this issue, the LiDO model innovatively proposes a three-layer refined verification framework:

1. Security abstraction layer: Mapping the protocol to a linearized state machine to ensure log consistency (security);
2. Activation Assurance Layer: Introduce the "Pacemaker" mechanism to solve the network delay problem through timeout broadcasting and round synchronization;
3. DAG Extension Layer: Supports emerging DAG protocols such as Narwhal and Bullshark, achieving efficient verification of leaderless Consensus.

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-phase BFT) and multiple DAG protocols, completing mechanized proofs of over 10,000 lines of Coq code, with safety and liveness verification code amounts reaching 4,000 lines and 1,700 lines respectively. The professor pointed out in his speech: "At present, PoS consensus protocols generally face the dilemma of being unable to achieve safety, liveness, and decentralization simultaneously. The LiDO model is a systematic design solution proposed to break this dilemma."

The professor once led a team to develop the world's first "bug-free" operating system CertiKOS, which is hailed as a "milestone in cyber-physical system security." This achievement not only laid a solid foundation for his deep accumulation in the field of system security but also established a basis for subsequent research in blockchain security.

LiDO has currently completed model design and formal verification, and has begun exploring the integration possibilities with mainstream public chains and decentralized protocols. The professor stated that they are committed to verifying key mechanisms in Web3.0 to provide full-cycle products and services, better supporting the long-term development strategy of Web3 enterprises and ecosystems. At the end of the speech, he emphasized: "A trustworthy, secure, and verifiable network protocol stack will be the key pathway to a truly decentralized future."