No cimeira de estudiosos do Web3, o professor de Yale revelou pela primeira vez o modelo LiDO

A Cimeira dos Acadêmicos de Web3 de 2025 foi realizada hoje, onde o professor Shao Zhong do departamento de ciência da computação da Universidade de Yale fez um discurso principal intitulado "Segurança e Prova de Atividade de Protocolos de Consenso Refinados: LiDO e sua Extensão". Ele apresentou pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de extensão LiDO-DAG. Este resultado inovador visa fornecer segurança e prova de 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 larga escala do ecossistema Web3.

O Professor Shao Zhong apontou em sua palestra que, apesar dos protocolos de consenso existentes como PBFT e Jolteon serem amplamente utilizados, a complexidade de implementação muitas vezes oculta vulnerabilidades potenciais. Para resolver esse 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 de Atividade: Introdução do mecanismo "Pacemaker" para resolver o problema de latência da rede através de transmissão de tempo limite e sincronização de rodadas;
3. Camada de expansão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, permitindo uma validação eficiente de 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 mais de 10.000 linhas de código Coq com prova mecanizada, com a quantidade de código para verificação de segurança e atividade alcançando 4.000 e 1.700 linhas, respectivamente. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam a difícil situação de não conseguir ter segurança, atividade e descentralização ao mesmo tempo. O modelo LiDO é uma proposta de design sistêmico destinada a romper essa situação."

Como o desenvolvedor do CertiKOS, o primeiro sistema operacional "sem vulnerabilidades" do mundo através de verificação formal, o Professor Zhao Zhong acumulou uma sólida experiência na área de segurança de sistemas. Este feito é considerado um "marco na segurança de sistemas ciber-físicos". Nos últimos anos, o Professor Zhao Zhong mudou seu foco de pesquisa para a segurança em blockchain e, em 2017, co-fundou uma empresa de segurança com seu aluno, o Professor Gu Ronghui, introduzindo a tecnologia de verificação formal na segurança de contratos inteligentes e protocolos on-chain, proporcionando proteção de segurança para ativos criptográficos de bilhões de dólares.

O modelo LiDO completou atualmente 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 mecanismos-chave no Web3.0, a fim de fornecer produtos e serviços de ciclo completo, apoiando melhor a estratégia de desenvolvimento a longo prazo das empresas e ecossistemas Web3.

No final da palestra, o Professor Shao Zhong enfatizou: "Um stack de protocolos de rede confiável, seguro e verificável será o caminho chave para um verdadeiro futuro descentralizado."