No cume da Web3, o professor de Yale apresentou pela primeira vez o modelo LiDO

Na recente Cimeira de Académicos Web3 de 2025, o Professor Zhao Zhong do Departamento de Ciência da Computação da Universidade de Yale fez uma apresentação intitulada "Prova de Segurança e Vitalidade de Protocolos de Consenso Baseados em Refinamento: LiDO e Sua Extensão", onde apresentou ao público pela primeira vez o modelo LiDO e a estrutura de extensão LiDO-DAG desenvolvidos por 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, pavimentando o caminho 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) sejam amplamente utilizados, frequentemente existem potenciais riscos de segurança devido à complexidade de sua implementação. Para resolver esse problema, o modelo LiDO propôs uma estrutura inovadora de validaçã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 e assegurando a segurança;
2. Camada de Garantia de Atividade: Introduz o mecanismo "Pacemaker" para resolver problemas de latência na rede através de transmissões de timeout e sincronização de turnos;
3. Camada de extensão DAG: suporta protocolos DAG emergentes como Narwhal e Bullshark, implementando uma verificação de consenso sem líder eficiente.

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, onde a quantidade de código para verificação de segurança e de atividade atingiu respectivamente 4000 linhas e 1700 linhas. O Professor Shao Zhong enfatizou em sua palestra: "Atualmente, os protocolos de consenso PoS enfrentam amplamente a dificuldade de equilibrar segurança, atividade e descentralização. O modelo LiDO é uma proposta de design sistêmico para romper essa dificuldade."

A equipe liderada pelo Professor Shao Zhong desenvolveu anteriormente o CertiKOS, que é o primeiro sistema operacional "sem falhas" do mundo validado formalmente, considerado pela indústria como um "marco na segurança de sistemas ciberfísicos". Essa conquista não apenas estabeleceu a base para as tecnologias relacionadas, mas também demonstrou a profunda acumulação da equipe no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong se aprofundou na pesquisa de segurança em blockchain e, em 2017, co-fundou uma empresa de segurança com colegas, introduzindo a tecnologia de validação formal na proteção de segurança de contratos inteligentes e protocolos on-chain, fornecendo proteção de segurança para ativos criptográficos no valor de centenas de bilhões.

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 dedicados a validar os mecanismos chave no Web3.0, para oferecer produtos e serviços com ciclo completo, apoiando melhor a estratégia de desenvolvimento a longo prazo de empresas e ecossistemas Web3. Ao final da apresentação, 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."