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

Na recente cimeira de académicos Web3 de 2025, o professor Shao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez uma palestra intitulada "Provas de segurança e vitalidade de protocolos de consenso refinados: LiDO e sua extensão", revelando pela primeira vez o modelo LiDO e a estrutura de extensão LiDO-DAG desenvolvidos pela sua equipe. Este resultado inovador visa fornecer provas de segurança e vitalidade verificáveis mecanicamente para protocolos de consenso de tolerância a falhas bizantinas (BFT) complexos, estabelecendo uma base técnica para a fiabilidade e desenvolvimento em larga escala do ecossistema Web3.

O professor Shao Zhong, em sua palestra, apontou que, apesar dos protocolos de consenso existentes (como PBFT, Jolteon) serem amplamente utilizados, sua complexidade de implementação frequentemente oculta vulnerabilidades potenciais. Para resolver esse problema, o modelo LiDO apresentou de forma inovadora uma estrutura de verificação refinada em três camadas:

1. Camada de abstração de segurança: mapeando o protocolo como uma máquina de estados linearizada, garantindo a consistência dos registros (segurança);
2. Camada de garantia de atividade: introduz o mecanismo "Pacemaker", resolvendo problemas de latência na rede através da difusão de tempo limite e sincronização de rondas;
3. Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, implementando uma validação eficiente sem consenso de 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 prova mecânica em Coq, onde a quantidade de código para verificação de segurança e de 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 o desafio comum de equilibrar segurança, vivacidade e descentralização. O modelo LiDO é uma solução sistemática proposta para superar esse impasse."

A equipe liderada pelo Professor Shao Zhong desenvolveu o CertiKOS, o primeiro sistema operacional "sem falhas" do mundo, validado formalmente, sendo considerado um "marco na segurança de sistemas ciber-físicos". Esta conquista não apenas estabeleceu uma base sólida para eles na área de segurança de sistemas, mas também demonstrou sua vasta experiência nesse campo. Nos últimos anos, o Professor Shao Zhong tem se concentrado na pesquisa de segurança em blockchain, e em 2017, fundou uma empresa de segurança com seus colegas, introduzindo a tecnologia de validação formal na proteção de segurança de contratos inteligentes e protocolos on-chain, oferecendo segurança para ativos criptográficos no valor 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 eles estão empenhados em validar mecanismos chave no Web3.0, a fim de fornecer produtos e serviços durante todo o ciclo, apoiando melhor as estratégias de desenvolvimento a longo prazo das empresas e ecossistemas Web3. Ao 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 futuro verdadeiramente descentralizado."