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

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 pronunció un discurso titulado "Prueba de seguridad y actividad de protocolos de consenso refinados: LiDO y su marco de expansión", donde 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, sentando una base tecnológica para la confiabilidad y el desarrollo a gran escala del ecosistema Web3.

El profesor Shao Zhong señaló que aunque los protocolos de consenso existentes son ampliamente utilizados, la complejidad de su implementación a menudo oculta vulnerabilidades potenciales. 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 como una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
2. Capa de garantía activa: Introducción del mecanismo "Pacemaker" para resolver el problema de la latencia en la red a través de la difusión por tiempo de espera y la sincronización de rondas;
3. Capa de extensión DAG: soporte para nuevos protocolos DAG, logrando una verificació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, completando la mecanización de pruebas 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, en su discurso, señaló: "En la actualidad, los protocolos de consenso PoS enfrentan generalmente la difícil situación de no poder lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es una propuesta de diseño sistemático para romper esta situación."

El CertiKOS, desarrollado por el profesor Shao Zhong y su equipo, es el primer sistema operativo "sin vulnerabilidades" del mundo que ha sido verificado formalmente, y ha sido considerado un "hito en la seguridad de los sistemas ciberfísicos". Este logro no solo establece su base técnica en el campo de la seguridad de sistemas, sino que también destaca su profunda acumulación de conocimientos. En los últimos años, el profesor Shao Zhong se ha enfocado en la seguridad de blockchain y, en 2017, junto con su discípulo el profesor Gu Ronghui, introdujo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo la seguridad de activos criptográficos valorados en 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 afirmó que se dedican a validar 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 Web3. Al final de la conferencia, el profesor Shao Zhong enfatizó: "Una pila de protocolos de red confiable, segura y verificable será la clave para el camino hacia un futuro verdaderamente descentralizado."