Na cúpula dos acadêmicos de Web3, o Professor Shao Zhong apresentou o modelo LiDO, promovendo a verificação da segurança do protocolo de consenso.

A Cimeira de Acadêmicos Web3 de 2025 foi realizada recentemente, e o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez uma palestra intitulada "Prova de Segurança e Atividade de Protocolo de Consenso Refinado: LiDO e suas Extensões". Ele revelou pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de extensão LiDO-DAG, que 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 confiabilidade e desenvolvimento em escala do ecossistema Web3.

O Professor Shao Zhong, na sua palestra, apontou que os atuais protocolos de consenso como PBFT e Jolteon, embora amplamente utilizados, frequentemente escondem vulnerabilidades potenciais devido à alta complexidade de implementação. Para resolver este problema, o modelo LiDO propôs de forma inovadora uma estrutura de verificação refinada em três camadas:

1. Camada de abstração de segurança: mapeia o protocolo como uma máquina de estados linearizada, garantindo a consistência dos logs (segurança);
2. Camada de Garantia Ativa: Introduz o mecanismo "Pacemaker" para resolver o problema de latência da rede através da difusão de tempo limite e sincronização de rodadas;
3. Camada de expansão DAG: suporta novos protocolos DAG como Narwhal e Bullshark, realizando uma verificação eficiente de consenso sem líderes.

Atualmente, o LiDO já foi aplicado com sucesso em protocolos de nível industrial como o Jolteon (BFT de duas fases) e em vários protocolos DAG, completando mais de dez mil linhas de provas mecanizadas em Coq, das quais a quantidade de código para validação de segurança e vivacidade atinge 4000 linhas e 1700 linhas, respectivamente. O Professor Shao Zhong enfatiza: "Atualmente, os protocolos de consenso PoS enfrentam geralmente a dificuldade de conciliar segurança, vivacidade e descentralização. O modelo LiDO é uma proposta de design sistêmico destinada a superar esse gargalo."

Como um dos principais desenvolvedores do CertiKOS, o primeiro sistema operacional "sem falhas" validado formalmente no mundo, o Professor Shao Zhong acumulou uma vasta experiência na área de segurança de sistemas. Esta conquista não apenas estabeleceu uma base sólida para suas pesquisas subsequentes, mas também destacou sua contribuição excepcional no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong direcionou seu foco de pesquisa para a segurança de blockchain e, em 2017, co-fundou uma empresa de segurança com parceiros, dedicada a aplicar técnicas de validação formal na garantia da segurança de contratos inteligentes e protocolos em cadeia, proporcionando proteção de segurança para ativos criptográficos no valor de centenas de bilhões.

O modelo LiDO já completou o design e a verificação formal, e começou a explorar a possibilidade de integração com as principais blockchains e protocolos descentralizados. O professor Shao Zhong afirmou que estão empenhados em validar os mecanismos chave no Web3.0, para oferecer produtos e serviços ao longo de todo o ciclo, apoiando melhor a estratégia de desenvolvimento a longo prazo das empresas e ecossistemas Web3. No final da palestra, o professor Shao Zhong enfatizou: "Pilhas de protocolo de rede confiáveis, seguras e verificáveis serão o caminho chave para um futuro verdadeiramente descentralizado."