O modelo LiDO revelado pela primeira vez na Cimeira de Académicos Web3: fornecendo verificação mecanizada para protocolos de consenso complexos

Na Cimeira de Académicos de Web3 de 2025, o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez um discurso intitulado "Prova de Segurança e Atividade de Protocolo de Consenso Refinado: LiDO e suas Extensões", onde revelou pela primeira vez o modelo LiDO desenvolvido por sua equipe e o framework de extensão LiDO-DAG. Este resultado inovador visa fornecer provas de segurança e atividade que possam ser verificadas mecanicamente para o protocolo de consenso de Tolerância a Falhas Bizantinas (BFT) complexo, estabelecendo uma base técnica para a fiabilidade e desenvolvimento em larga escala do ecossistema Web3.

O Professor Shao Zhong apontou em sua palestra que, embora os protocolos de consenso existentes (como PBFT, Jolteon) tenham sido amplamente aplicados, 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 Ativa: Introduz o mecanismo "Pacemaker", resolvendo o problema de latência na 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 validação eficiente do consenso sem líderes.

Atualmente, o LiDO foi aplicado com sucesso em protocolos industriais como o Jolteon (BFT de duas fases) e vários protocolos DAG, completando mais de 10.000 linhas de provas mecanizadas em Coq, das quais as linhas de código para verificação de segurança e de atividade chegam a 4.000 e 1.700, respetivamente. O Professor Shao Zhong enfatiza: "Atualmente, os protocolos de consenso PoS enfrentam amplamente o dilema de não conseguir obter segurança, atividade e descentralização ao mesmo tempo. O modelo LiDO foi proposto precisamente como uma solução de design sistemático para quebrar esse dilema."

Como principal desenvolvedor do CertiKOS, o primeiro sistema operacional "sem falhas" do mundo por meio de verificação formal, o professor Zhao Zhong acumulou uma vasta experiência na área de segurança de sistemas. Esta conquista não apenas consolidou sua posição no campo da tecnologia de segurança, mas também destacou a capacidade profissional de sua equipe em segurança de sistemas. Nos últimos anos, o professor Zhao Zhong voltou seu foco de pesquisa para a segurança em blockchain e, em 2017, co-fundou uma empresa focada em segurança de blockchain com seus parceiros, introduzindo a tecnologia de verificação formal na proteção de 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 foi atualmente projetado e validado formalmente, 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 fornecer produtos e serviços de ciclo completo, apoiando melhor a estratégia de desenvolvimento de 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."