Se revela por primera vez el modelo LiDO en la Cumbre de Académicos de Web3: proporciona verificación mecanizada para protocolos de consenso complejos

En la Cumbre de Académicos de Web3 de 2025, el profesor Shao Zhong del departamento de ciencias de la computación de la Universidad de Yale dio una conferencia titulada "Prueba de seguridad y actividad de un protocolo de consenso refinado: LiDO y su marco de expansión". En esta conferencia, presentó por primera vez el modelo LiDO desarrollado por su equipo y el marco de expansión LiDO-DAG. Este resultado innovador tiene como objetivo proporcionar pruebas de seguridad y actividad verificables mecánicamente para protocolos de consenso de tolerancia 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 han aplicado ampliamente, a menudo ocultan vulnerabilidades potenciales debido a su complejidad de implementación. Para abordar este problema, el modelo LiDO propone de manera innovadora un marco de verificación refinada en tres niveles:

1. Capa de abstracción de seguridad: mapea el protocolo como una máquina de estados linealizada, asegurando la consistencia 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 nuevos protocolos DAG como Narwhal y Bullshark, logrando una validación eficiente sin un líder en el consenso.

Actualmente, LiDO se ha aplicado con éxito en el protocolo industrial Jolteon (BFT de dos fases) y en múltiples protocolos DAG, completando la prueba mecánica de más de diez mil líneas de código Coq, donde la cantidad de código para la verificación de seguridad y actividad alcanza 4000 líneas y 1700 líneas, respectivamente. El profesor Shao Zhong enfatizó: "En la actualidad, los protocolos de consenso PoS enfrentan comúnmente la difícil situación de lograr seguridad, actividad y descentralización a la vez. El modelo LiDO es una propuesta de diseño sistemático para romper esta dificultad."

Como principal desarrollador del sistema operativo CertiKOS, el primer sistema operativo "sin vulnerabilidades" del mundo que ha pasado por una verificación formal, el profesor Zhao Zhong ha acumulado una profunda experiencia en el campo de la seguridad de sistemas. Este logro no solo ha consolidado su posición en el campo de la tecnología de seguridad, sino que también ha destacado la capacidad profesional de su equipo en la seguridad de sistemas. En los últimos años, el profesor Zhao Zhong ha trasladado su enfoque de investigación hacia la seguridad de blockchain y, en 2017, cofundó una empresa centrada en la seguridad de blockchain con sus socios, introduciendo la tecnología de verificación formal para garantizar la seguridad de los contratos inteligentes y los protocolos en cadena, proporcionando protección de seguridad para activos criptográficos de cientos de miles de millones de dólares.

El modelo LiDO ha completado su diseño y 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 dedicados a verificar los mecanismos clave en Web3.0 para ofrecer 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."