En la cumbre de académicos de Web3 se presentó por primera vez el modelo LiDO, ofreciendo nuevas ideas para la seguridad del protocolo de consenso.

En la reciente Cumbre de Académicos Web3 2025, un profesor del Departamento de Ciencias de la Computación de la Universidad de Yale pronunció una conferencia titulada "Prueba de seguridad y actividad del protocolo de consenso refinado: LiDO y su marco de expansión", presentando por primera vez al público el modelo LiDO y el marco de expansión LiDO-DAG desarrollado por su equipo. Este innovador logro tiene como objetivo proporcionar pruebas verificables mecánicamente de seguridad y actividad para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, sentando las bases técnicas para la fiabilidad y el desarrollo a gran escala del ecosistema Web3.

El profesor señaló en su discurso que, a pesar de que los protocolos de consenso existentes (como PBFT, Jolteon) se han utilizado ampliamente, a menudo ocultan vulnerabilidades de seguridad potenciales debido a la alta complejidad de implementación. Para abordar este problema, el modelo LiDO propuso 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 consistencia de los registros (seguridad);
2. Capa de garantía activa: Introducir el mecanismo "Pacemaker" para resolver el problema de latencia de la red a través de la difusión de 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 verificación eficiente del consenso sin 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 más de diez mil líneas de código Coq con pruebas mecanizadas, donde la cantidad de código para la verificación de seguridad y actividad alcanzó las 4000 líneas y 1700 líneas, respectivamente. El profesor enfatizó en la conferencia: "En la actualidad, los protocolos de consenso PoS enfrentan comúnmente el dilema de no poder lograr simultáneamente seguridad, actividad y descentralización. El modelo LiDO es precisamente un plan de diseño sistemático propuesto para superar este cuello de botella."

Cabe mencionar que este profesor anteriormente lideró un equipo que desarrolló el primer sistema operativo "sin vulnerabilidades" CertiKOS a través de la verificación formal, el cual ha sido aclamado en la industria como un "hito en la seguridad de sistemas ciberfísicos". Este logro no solo sentó las bases técnicas para la empresa de seguridad que fundó posteriormente, sino que también mostró su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, este profesor ha investigado a fondo la seguridad de blockchain, introduciendo 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 por un valor de cientos de miles de millones de dólares.

El modelo LiDO ha completado actualmente su diseño y verificación formal, y ha comenzado a explorar la posibilidad de integración con cadenas de bloques públicas y protocolos descentralizados de referencia. El profesor indicó 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 su discurso, enfatizó: "Una pila de protocolos de red confiable, segura y verificable, será el camino clave hacia un futuro verdaderamente descentralizado."