Cimeira dos Académicos Web3 em Debate: Professor de Yale Revela pela Primeira Vez o Modelo LiDO

Na recente Cimeira de Académicos Web3 de 2025, o Professor Zhao Zhong do Departamento de Ciências da Computação da Universidade de Yale fez uma apresentação sobre "Prova de Segurança e Atividade de Protocolos de Consenso Refinados: LiDO e a sua Expansão", introduzindo ao público pela primeira vez o modelo LiDO e a estrutura expandida 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 tolerantes a falhas bizantinas (BFT) complexos, estabelecendo uma base técnica para a fiabilidade e desenvolvimento em grande escala do ecossistema Web3.

O professor Shao Zhong, na sua palestra, apontou que, apesar de os atuais protocolos de consenso (como PBFT, Jolteon) serem amplamente utilizados, frequentemente escondem vulnerabilidades potenciais devido à complexidade de implementação. Para resolver esse problema, o modelo LiDO propôs uma estrutura inovadora de verificação em três camadas:

1. Camada de abstração de segurança: mapeia protocolos como máquinas de estado linearizadas, garantindo a consistência dos logs (segurança);
2. Camada de Garantia de Atividade: Introdução do mecanismo "Pacemaker", que resolve problemas de latência de rede através de difusão de tempo limite e sincronização de rodadas;
3. Camada de extensão DAG: suporte a novos protocolos DAG emergentes como Narwhal e Bullshark, permitindo a verificação eficiente de 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 provas mecanizadas em Coq, nas quais as linhas de código para verificação de segurança e de vivacidade somam, respetivamente, 4000 e 1700 linhas. O Professor Shao Zhong enfatizou na palestra: "Atualmente, os protocolos de consenso PoS enfrentam geralmente a dificuldade de conciliar segurança, vivacidade e descentralização. O modelo LiDO foi proposto como uma solução de design sistêmico para romper essa dificuldade."

Vale a pena mencionar que a CertiKOS, desenvolvida pela equipe liderada pelo Professor Shao Zhong, é o primeiro sistema operacional "sem vulnerabilidades" do mundo a passar por verificação formal, sendo aclamado pela indústria como um "marco na segurança de sistemas ciberfísicos". Esta conquista não só destaca sua profunda experiência na área de segurança de sistemas, mas também estabelece uma base sólida para futuras pesquisas em segurança de blockchain. Desde 2017, o Professor Shao Zhong tem se dedicado a introduzir a tecnologia de verificação formal na área de garantia de segurança de contratos inteligentes e protocolos on-chain, contribuindo significativamente para a proteção da segurança de ativos criptográficos no valor de centenas de bilhões de dólares.

Atualmente, o LiDO completou o design do modelo e a verificação formal, e começou a explorar a possibilidade de integração com cadeias públicas mainstream e protocolos descentralizados. O Professor Shao Zhong afirmou que eles estão empenhados em validar os mecanismos-chave no Web3.0, a fim de oferecer produtos e serviços de ciclo completo, apoiando melhor a estratégia de desenvolvimento de longo prazo de 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 fundamental para um futuro verdadeiramente descentralizado."