En la cumbre de académicos de Web3, el profesor de Yale presenta por primera vez el modelo LiDO

En la reciente Cumbre de Académicos Web3 2025, el profesor Shao Zhong del Departamento de Ciencias de la Computación de la Universidad de Yale presentó una conferencia titulada "Pruebas de seguridad y vitalidad de protocolos de consenso refinados: LiDO y su marco de expansión", revelando por primera vez el modelo LiDO desarrollado por su equipo y el marco de expansión LiDO-DAG. Este innovador resultado tiene como objetivo proporcionar pruebas de seguridad y vitalidad verificables mecánicamente para complejos protocolos de consenso tolerantes a fallos bizantinos (BFT), sentando así 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, Jolteon) se utilizan 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 de tres capas:

1. Capa de abstracción de seguridad: mapea el protocolo a una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
2. Capa de garantía activa: introduce el mecanismo "Pacemaker" para resolver el problema de la latencia de la red mediante la difusión de 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 validación eficiente sin consenso de líderes.

Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos fases) y en múltiples protocolos DAG, habiendo completado más de 10,000 líneas de código Coq con pruebas mecanizadas, donde la cantidad de código para la verificación de seguridad y de actividad alcanza respectivamente 4,000 y 1,700 líneas. El profesor Shao Zhong enfatizó en su discurso: "En la actualidad, los protocolos de consenso PoS enfrentan el desafío de equilibrar la seguridad, la actividad y la descentralización. El modelo LiDO es una solución sistemática propuesta para superar este dilema."

El equipo liderado por el profesor Shao Zhong desarrolló CertiKOS, el primer sistema operativo "sin vulnerabilidades" del mundo, validado formalmente, y se considera un "hito en la seguridad de sistemas ciberfísicos". Este logro no solo establece una sólida base en el campo de la seguridad de sistemas, sino que también demuestra su rica experiencia en este ámbito. En los últimos años, el profesor Shao Zhong se ha centrado en la investigación de seguridad en blockchain y en 2017 cofundó una empresa de seguridad con colegas, introduciendo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, ofreciendo protección de seguridad para activos criptográficos valorados en cientos de miles de millones de dólares.

LiDO ha completado actualmente el diseño del modelo y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas de bloques públicas y protocolos descentralizados. El profesor Shao Zhong expresó que están comprometidos 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 presentación, el profesor Shao Zhong enfatizó: "Un stack de protocolos de red confiables, seguros y verificables será el camino clave hacia un futuro verdaderamente descentralizado."