Cumbre de académicos de Web3: el profesor de Yale presenta un modelo innovador de verificación de consenso
La cumbre de académicos Web3 de 2025 se llevó a cabo recientemente, y el profesor Shao Zhong del departamento de ciencias de la computación de la Universidad de Yale dio una conferencia magistral, presentando 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 una seguridad y pruebas de actividad verificables mecánicamente para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, estableciendo 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, aunque los protocolos de consenso existentes se aplican ampliamente, su complejidad de 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.
Capa de abstracción segura: mapea el protocolo como una máquina de estados linealizada, asegurando la consistencia de los registros (seguridad);
Capa de garantía activa: Introducción del mecanismo "Pacemaker" para resolver el problema de la latencia de la red a través de la difusión de tiempo de espera y sincronización de rondas;
Capa de expansión DAG: soporta nuevos protocolos DAG, realizando una verificación eficiente con consenso sin líderes.
Actualmente, LiDO se ha aplicado con éxito en protocolos de nivel industrial y en múltiples protocolos DAG, completando la prueba mecanizada de más de diez mil líneas de código Coq, con una cantidad de código de verificación de seguridad y vitalidad que alcanza las 4000 y 1700 líneas, respectivamente. El profesor Shao Zhong señaló en su discurso: "En la actualidad, los protocolos de consenso PoS enfrentan comúnmente la difícil situación de no poder lograr simultáneamente seguridad, vitalidad y descentralización. El modelo LiDO es un plan de diseño sistemático propuesto precisamente 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 ha establecido la base técnica de su empresa, sino que también resalta su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, el profesor Shao Zhong se ha centrado en la seguridad blockchain, y en 2017 cofundó una empresa con su discípulo, el profesor Gu Ronghui, introduciendo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo la seguridad de activos criptográficos de nivel de miles de millones de dólares.
LiDO ha completado el diseño del modelo y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas públicas y protocolos descentralizados. El profesor Shao Zhong expresó que están dedicados a validar 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ó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado."
Esta página puede contener contenido de terceros, que se proporciona únicamente con fines informativos (sin garantías ni declaraciones) y no debe considerarse como un respaldo por parte de Gate a las opiniones expresadas ni como asesoramiento financiero o profesional. Consulte el Descargo de responsabilidad para obtener más detalles.
El profesor de Yale publica el modelo LiDO, superando el desafío de verificación del protocolo de consenso de Web3.
Cumbre de académicos de Web3: el profesor de Yale presenta un modelo innovador de verificación de consenso
La cumbre de académicos Web3 de 2025 se llevó a cabo recientemente, y el profesor Shao Zhong del departamento de ciencias de la computación de la Universidad de Yale dio una conferencia magistral, presentando 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 una seguridad y pruebas de actividad verificables mecánicamente para protocolos de consenso tolerantes a fallos bizantinos (BFT) complejos, estableciendo 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, aunque los protocolos de consenso existentes se aplican ampliamente, su complejidad de 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.
Actualmente, LiDO se ha aplicado con éxito en protocolos de nivel industrial y en múltiples protocolos DAG, completando la prueba mecanizada de más de diez mil líneas de código Coq, con una cantidad de código de verificación de seguridad y vitalidad que alcanza las 4000 y 1700 líneas, respectivamente. El profesor Shao Zhong señaló en su discurso: "En la actualidad, los protocolos de consenso PoS enfrentan comúnmente la difícil situación de no poder lograr simultáneamente seguridad, vitalidad y descentralización. El modelo LiDO es un plan de diseño sistemático propuesto precisamente 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 ha establecido la base técnica de su empresa, sino que también resalta su profunda acumulación en el campo de la seguridad de sistemas. En los últimos años, el profesor Shao Zhong se ha centrado en la seguridad blockchain, y en 2017 cofundó una empresa con su discípulo, el profesor Gu Ronghui, introduciendo la tecnología de verificación formal en la seguridad de contratos inteligentes y protocolos en cadena, protegiendo la seguridad de activos criptográficos de nivel de miles de millones de dólares.
LiDO ha completado el diseño del modelo y la verificación formal, y ha comenzado a explorar la posibilidad de integración con las principales cadenas públicas y protocolos descentralizados. El profesor Shao Zhong expresó que están dedicados a validar 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ó: "Una pila de protocolos de red confiable, segura y verificable será el camino clave hacia un futuro verdaderamente descentralizado."