No cimeira de estudiosos da Web3, o professor de Yale partilha os avanços na pesquisa sobre a segurança do protocolo de consenso.

Na Cimeira de Académicos Web3 de 2025, o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale apresentou uma palestra intitulada "Provas de Segurança e Atividade de Protocolo de Consenso Refinado: LiDO e a sua Expansão", onde divulgou pela primeira vez o modelo LiDO desenvolvido pela sua equipa e a estrutura de expansão LiDO-DAG. Este resultado inovador visa fornecer provas de segurança e atividade verificáveis mecanicamente para protocolos de consenso de Tolerância a Falhas Bizantinas (BFT) complexos, estabelecendo uma base técnica para a fiabilidade e desenvolvimento em grande escala do ecossistema Web3.

O professor Shao Zhong apontou em sua palestra que os protocolos de consenso existentes (como PBFT, Jolteon), embora amplamente utilizados, muitas vezes escondem vulnerabilidades potenciais devido à sua complexidade de implementação. Para resolver esse problema, o modelo LiDO propôs de forma inovadora uma estrutura de validação refinada em três camadas:

1. Camada de abstração segura: mapeia o protocolo como uma máquina de estados linearizada, garantindo a consistência dos logs (segurança);
2. Camada de Garantia de Atividade: Introduzindo o mecanismo "Pacemaker", que resolve o problema de latência da rede através de difusão de tempo limite e sincronização de rodadas;
3. Camada de extensão DAG: suporta novos protocolos DAG emergentes como Narwhal e Bullshark, permitindo a verificação eficiente do consenso sem líder.

Atualmente, o LiDO foi aplicado com sucesso no protocolo industrial Jolteon (BFT de duas fases) e em vários protocolos DAG, completando a prova mecanizada de mais de 10.000 linhas de código Coq, com a quantidade de código para validação de segurança e atividade alcançando 4.000 linhas e 1.700 linhas, respectivamente. O professor Shao Zhong apontou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam amplamente a dificuldade de garantir segurança, atividade e descentralização ao mesmo tempo. O modelo LiDO é uma proposta de design sistemático para romper esse dilema."

Vale a pena mencionar que o CertiKOS, desenvolvido pela equipe liderada pelo Professor Shao Zhong, é o primeiro sistema operacional "sem vulnerabilidades" do mundo a ser validado por meio de verificação formal, sendo considerado um "marco na segurança de sistemas ciberfísicos". Esta conquista não apenas estabelece uma base sólida para suas profundas contribuições no campo da segurança de sistemas, mas também fornece uma base firme para futuras pesquisas em segurança de blockchain. Em 2017, o Professor Shao Zhong e seu discípulo, o Professor Gu Ronghui, introduziram a tecnologia de verificação formal na segurança de contratos inteligentes e protocolos on-chain, oferecendo suporte importante para a segurança de ativos criptográficos.

LiDO atualmente completou o design do modelo e a verificação formal, e começou a explorar a possibilidade de integração com cadeias públicas mainstream e protocolos descentralizados. O professor Shao Zhong afirmou que estão dedicados a validar mecanismos chave no Web3.0 para fornecer produtos e serviços de ciclo completo, apoiando melhor as estratégias de desenvolvimento de longo prazo das empresas e ecossistemas Web3. No final da palestra, o professor Shao Zhong enfatizou: "Uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um verdadeiro futuro descentralizado."