No cimeira dos académicos de Web3, o modelo LiDO é revelado pela primeira vez, oferecendo novas ideias para a segurança do protocolo de consenso.

Na recente cimeira de académicos Web3 de 2025, um professor do departamento de ciência da computação da Universidade de Yale fez um discurso intitulado "Prova de segurança e atividade de protocolos de consenso refinados: LiDO e sua extensão", apresentando ao público pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de extensão LiDO-DAG. Este resultado inovador visa fornecer provas de segurança e atividade verificáveis mecanicamente para protocolos de consenso Byzantine Fault Tolerance (BFT) complexos, estabelecendo uma base técnica para a fiabilidade e o desenvolvimento em grande escala do ecossistema Web3.

O professor apontou em sua palestra que, embora os protocolos de consenso existentes (como PBFT, Jolteon) tenham sido amplamente utilizados, a alta complexidade de implementação muitas vezes oculta vulnerabilidades de segurança 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: Introdução do mecanismo "Pacemaker", que resolve o problema de latência da rede através da difusão de tempo limite e sincronização de rodadas;
3. Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal, Bullshark, permitindo uma validaçã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 mais de dez mil linhas de código Coq com prova mecanizada, nas quais a quantidade de código para verificação de segurança e de vivacidade alcançou 4000 linhas e 1700 linhas, respectivamente. O professor enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam amplamente a dificuldade de garantir segurança, vivacidade e descentralização ao mesmo tempo. O modelo LiDO foi proposto como uma solução de design sistêmico para superar esse gargalo."

Vale a pena mencionar que este professor anteriormente liderou uma equipa que desenvolveu o primeiro sistema operativo "sem falhas" do mundo através de verificação formal, chamado CertiKOS, que foi aclamado pela indústria como um "marco na segurança de sistemas ciberfísicos". Este feito não apenas estabeleceu a base técnica para a empresa de segurança que ele fundou posteriormente, mas também demonstrou seu profundo conhecimento na área de segurança de sistemas. Nos últimos anos, o professor aprofundou sua pesquisa em segurança de blockchain, introduzindo técnicas de verificação formal no campo da segurança de contratos inteligentes e protocolos em cadeia, fornecendo proteção de segurança para ativos criptográficos avaliados em centenas de bilhões de dólares.

O modelo LiDO foi atualmente concluído 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 afirmou que estão dedicados a validar mecanismos-chave na 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, ele enfatizou: "Um stack de protocolos de rede confiável, seguro e verificável será o caminho chave para um futuro verdadeiramente descentralizado."