En la cumbre de académicos de Web3, el profesor de Yale presentó públicamente el modelo LiDO por primera vez.

La Cumbre de Académicos de Web3 de 2025 se celebró hoy, el profesor Shao Zhong del Departamento de Ciencias de la Computación de la Universidad de Yale pronunció una conferencia titulada "Prueba de Seguridad y Vitalidad de Protocolos de Consenso Refinados: LiDO y sus Extensiones". Presentó por primera vez el modelo LiDO desarrollado por su equipo y el marco de extensión LiDO-DAG. Este logro innovador busca proporcionar pruebas de seguridad y vitalidad verificables mecánicamente para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, sentando una base técnica para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.

El profesor Shao Zhong señaló en su discurso que, a pesar de que los protocolos de consenso existentes como PBFT y Jolteon se aplican ampliamente, a menudo ocultan vulnerabilidades potenciales debido a la complejidad de su implementación. Para abordar este problema, el modelo LiDO propone de manera innovadora un marco de verificación refinado en tres capas:

1. Capa de abstracción de seguridad: mapea el protocolo como una máquina de estados linealizada, asegurando la coherencia de los registros (seguridad);
2. Capa de garantía activa: se introduce el mecanismo "Pacemaker" para resolver el problema de la latencia de la red a través de la difusión por tiempo de espera y la sincronización de rondas;
3. Capa de expansión DAG: soporta protocolos DAG emergentes como Narwhal y Bullshark, logrando una verificación eficiente de consenso sin líderes.

Actualmente, LiDO se ha implementado con éxito en el protocolo industrial Jolteon (BFT de dos fases) y en varios protocolos DAG, completando la prueba mecánica de más de diez mil líneas de código Coq, con una cantidad de código para la verificación de seguridad y actividad que alcanza las 4000 y 1700 líneas, respectivamente. El profesor Shao Zhong enfatizó en su discurso: "En la actualidad, los protocolos de consenso PoS enfrentan la difícil situación de no poder obtener simultáneamente seguridad, actividad y descentralización. El modelo LiDO es un esquema de diseño sistemático propuesto para romper esta situación."

Como el desarrollador de CertiKOS, el primer sistema operativo "sin vulnerabilidades" del mundo que ha sido verificado formalmente, el profesor Shao Zhong ha acumulado una profunda experiencia en el campo de la seguridad de sistemas. Este logro ha sido calificado como "un hito en la seguridad de sistemas ciberfísicos". En los últimos años, el profesor Shao Zhong ha dirigido su investigación hacia la seguridad en blockchain, y en 2017, junto con su discípulo el profesor Gu Ronghui, fundó una empresa de seguridad que introduce la tecnología de verificación formal en la garantía de seguridad de contratos inteligentes y protocolos en cadena, proporcionando protección de seguridad para activos criptográficos valorados en cientos de miles de millones.

El modelo LiDO ha completado actualmente su diseño y validación formal, y ha comenzado a explorar la posibilidad de integración con cadenas de bloques principales y protocolos descentralizados. El profesor Shao Zhong expresó que están dedicados a verificar los mecanismos clave en Web3.0 para proporcionar productos y servicios de ciclo completo, apoyando mejor la estrategia de desarrollo a largo plazo de las empresas y ecosistemas de Web3.

Al final de la charla, el profesor Shao Zhong enfatizó: "Un stack de protocolos de red que sea confiable, seguro y verificable, será el camino clave hacia un futuro verdaderamente descentralizado."