O Professor de Yale apresenta pela primeira vez o modelo LiDO na Cimeira dos Académicos Web3

Na Cimeira dos Académicos de Web3 de 2025, 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 Suas Expansões", onde apresentou pela primeira vez o modelo LiDO e a estrutura de expansão LiDO-DAG desenvolvidos pela sua equipa. Este resultado inovador visa fornecer provas de segurança e atividade que possam ser verificadas 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 que, embora os protocolos de consenso existentes sejam amplamente utilizados, a sua implementação complexa frequentemente oculta vulnerabilidades potenciais. Para resolver este 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", que resolve o problema da latência da rede através da transmissão de tempo limite e sincronização de rodadas;
3. Camada de extensão DAG: suporta novos protocolos DAG, 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 dez mil linhas de código Coq com provas mecanizadas, com a quantidade de código de verificação de segurança e atividade alcançando 4000 linhas e 1700 linhas, respectivamente. O Professor Shao Zhong, em sua palestra, apontou: "Atualmente, os protocolos de consenso PoS enfrentam geralmente a dificuldade de conciliar segurança, atividade e descentralização. O modelo LiDO é uma proposta de design sistêmico para quebrar essa dificuldade."

O CertiKOS, desenvolvido pela equipe liderada pelo Professor Shao Zhong, é o primeiro sistema operacional "sem falhas" do mundo que passou por verificação formal, sendo considerado um "marco na segurança de sistemas ciberfísicos". Esta conquista não apenas estabeleceu sua base técnica no campo da segurança de sistemas, mas também destacou sua profunda acumulação. Nos últimos anos, o Professor Shao Zhong tem se aprofundado na segurança de blockchain e, em 2017, em colaboração com seu aluno, o Professor Gu Ronghui, introduziu a tecnologia de verificação formal na segurança de contratos inteligentes e protocolos on-chain, garantindo a segurança de ativos criptográficos de bilhões de dólares.

A 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 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 a longo prazo das empresas e ecossistemas Web3. No final da palestra, o Professor Shao Zhong enfatizou: "Um stack de protocolos de rede confiáveis, seguros e verificáveis será o caminho chave para um futuro verdadeiramente descentralizado."