El cofundador de CertiK, el profesor Shao Zhong, asistió a la cumbre de académicos de Web3 y presentó por primera vez el modelo LiDO.

En la Conferencia de Académicos Web3 2025, que se llevó a cabo hoy, el profesor del departamento de ciencias de la computación de la Universidad de Yale y cofundador de CertiK, Zhao Zhong, pronunció un discurso titulado “Prueba de seguridad y actividad de protocolos de consenso refinados: LiDO y su expansión”. En este evento, presentó por primera vez el modelo LiDO y el marco de expansión LiDO-DAG desarrollado por su equipo. Este logro innovador tiene como objetivo proporcionar pruebas de seguridad y actividad verificables mecánicamente para protocolos de consenso de tolerancia a fallos bizantinos (BFT) complejos, estableciendo una base técnica para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.

En esta charla, el profesor Shao Zhong señaló que los protocolos de consenso existentes (como PBFT, Jolteon), aunque son ampliamente utilizados, 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 de tres capas:

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

Actualmente, LiDO se ha aplicado con éxito a protocolos industriales como Jolteon (BFT de dos fases) y a varios protocolos DAG, completando la prueba mecánica de más de diez mil líneas de código Coq, con un volumen de código de verificación de seguridad y de actividad que alcanzan las 4000 y 1700 líneas, respectivamente. “En la actualidad, los protocolos de consenso PoS enfrentan la difícil situación de no poder lograr simultáneamente seguridad, actividad y descentralización”, señaló el profesor Shao Zhong en su discurso. “El modelo LiDO es precisamente un plan de diseño sistemático propuesto para superar esta dificultad.”

El CertiKOS, desarrollado por el profesor Shao Zhong y su equipo, es el primer sistema operativo “sin vulnerabilidades” del mundo que ha sido validado formalmente, y ha sido aclamado como un “hito en la seguridad de sistemas ciberfísicos”. Este logro no solo establece la base técnica de la empresa de seguridad CertiK, sino que también destaca su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, el profesor Shao Zhong se ha dedicado a la seguridad de blockchain, y en 2017 cofundó CertiK junto con su discípulo el profesor Gu Ronghui, introduciendo la tecnología de validación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo así la seguridad de activos criptográficos de 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 cadenas de bloques públicas y protocolos descentralizados de vanguardia. El profesor Shao Zhong expresó que CertiK se dedica a verificar los mecanismos clave en Web3.0 para proporcionar productos y servicios a lo largo de todo el ciclo, 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 confiable, seguro y verificable será el camino clave hacia un futuro verdaderamente descentralizado.”