O cofundador da CertiK, Professor Zhao Zhong, participou da Cimeira de Académicos Web3, apresentando pela primeira vez o modelo LiDO.

Na conferência Web3 Scholars Conference 2025, realizada hoje, o professor do Departamento de Ciência da Computação da Universidade de Yale e cofundador da CertiK, Zhao Zhong, proferiu uma palestra intitulada “Segurança e prova de vitalidade de protocolos de consenso refinados: LiDO e sua expansão”. Ele apresentou pela primeira vez o modelo LiDO desenvolvido por sua equipe e a estrutura de expansão LiDO-DAG. Este resultado inovador visa fornecer segurança e prova de vitalidade verificáveis mecanicamente para protocolos de consenso de tolerância a falhas bizantinas complexas (BFT), estabelecendo uma base técnica para a confiabilidade e desenvolvimento em escala do ecossistema Web3.

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

• Camada de abstração de segurança: mapeia protocolos como máquinas de estado linearizadas, garantindo a consistência dos logs (segurança);
• Camada de Garantia Ativa: Introduz o mecanismo “Pacemaker”, que resolve o problema de latência na rede através da transmissão em tempo excessivo e sincronização de rondas;
• Camada de extensão DAG: suporta novos protocolos DAG emergentes como Narwhal, Bullshark, permitindo a validaçã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 a prova mecanizada de mais de dez mil linhas de código Coq, com a quantidade de código para verificação de segurança e atividade atingindo 4000 linhas e 1700 linhas, respectivamente. “Atualmente, os protocolos de consenso PoS enfrentam geralmente a difícil situação de não conseguir ter segurança, atividade e descentralização ao mesmo tempo”, apontou o professor Shao Zhong em sua palestra. “O modelo LiDO foi proposto como uma solução de design sistêmica para romper essa dificuldade.”

O CertiKOS, desenvolvido pela equipe liderada pelo Professor Shao Zhong, é o primeiro sistema operacional “sem vulnerabilidades” validado formalmente no mundo, sendo considerado um “marco na segurança de sistemas ciberfísicos”. Esta conquista não só estabeleceu a base técnica da empresa de segurança CertiK, mas também destacou sua profunda acumulação no campo da segurança de sistemas. Nos últimos anos, o Professor Shao Zhong tem se aprofundado na segurança de blockchain e, em 2017, co-fundou a CertiK com seu aluno, o Professor Gu Ronghui, introduzindo a tecnologia de validação formal na segurança de contratos inteligentes e protocolos on-chain, protegendo a segurança de ativos criptográficos de bilhões de dólares.

LiDO já concluiu o design do modelo e a verificação formal, e começou a explorar a possibilidade de integração com blockchains mainstream e protocolos descentralizados. O professor Shao Zhong afirmou que a CertiK está empenhada em verificar os mecanismos-chave na Web3.0, para fornecer produtos e serviços em todo o ciclo, apoiando melhor a estratégia de desenvolvimento a longo prazo para empresas e ecossistemas Web3. No final da apresentação, o professor Shao Zhong enfatizou: “Uma pilha de protocolos de rede confiável, segura e verificável será o caminho chave para um futuro verdadeiramente descentralizado.”