No cimeira de académicos Web3, o professor de Yale revelou pela primeira vez o modelo LiDO

A Cimeira de Acadêmicos Web3 de 2025 foi realizada recentemente, onde o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez uma palestra intitulada "Segurança e Prova de Atividade de Protocolos de Consenso Refinados: LiDO e sua Extensão", revelando 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 complexos de Tolerância a Falhas Bizantinas (BFT), estabelecendo uma base técnica para o desenvolvimento da confiabilidade e escalabilidade 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, sua complexidade de implementação frequentemente 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 Ativa: Introduz o mecanismo "Pacemaker" para resolver problemas de latência na rede através de difusã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íderes.

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 provas mecanizadas em Coq, onde a quantidade de código para verificação de segurança e vivacidade atingiu respectivamente 4.000 linhas e 1.700 linhas. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam universalmente a dificuldade de equilibrar segurança, vivacidade e descentralização. O modelo LiDO é uma proposta de design sistemático para romper essa dificuldade."

O CertiKOS, desenvolvido anteriormente pelo Professor Shao Zhong e sua equipe, é o primeiro sistema operacional "sem falhas" do mundo validado por verificação formal, sendo considerado um "marco na segurança de sistemas ciberfísicos". Essa conquista não apenas estabelece sua profunda base no campo da segurança de sistemas, mas também demonstra sua capacidade profissional nesse domínio. Nos últimos anos, o Professor Shao Zhong tem se aprofundado na pesquisa de segurança em blockchain e, em 2017, juntamente com seu aluno, o Professor Gu Ronghui, introduziu a tecnologia de verificação formal na área de proteção de segurança de contratos inteligentes e protocolos on-chain, oferecendo proteção de segurança para ativos criptográficos na ordem de centenas de bilhões de dólares.

LiDO já completou o design do modelo 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 dedicados a validar os mecanismos-chave na Web3.0 para oferecer produtos e serviços de ciclo completo, apoiando melhor a estratégia de desenvolvimento a longo prazo das empresas e ecossistemas Web3. Ao finalizar a palestra, o professor Shao Zhong enfatizou: "Uma pilha de protocolos de rede confiável, segura e verificável será o caminho-chave para um futuro verdadeiramente descentralizado."