На саммите ученых Web3 профессор Йельского университета впервые представил модель LiDO

С недавнего времени в 2025 году состоялся Саммит ученых Web3, на котором профессор кафедры компьютерных наук Йельского университета Чжао Чжун выступил с основной речью на тему «Безопасность и доказательство активности усовершенствованного согласованного протокола: LiDO и его расширение», впервые раскрыв свою команду разработанную модель LiDO и расширяющую инфраструктуру LiDO-DAG. Этот инновационный результат призван обеспечить механизируемую проверку безопасности и доказательства активности для сложных протоколов согласования с байесовской стойкостью (BFT), закладывая технологическую основу для надежности и масштабируемости экосистемы Web3.

Профессор Шао Чжун в своем выступлении отметил, что, хотя существующие протоколы согласия (такие как PBFT и Jolteon) широко применяются, они часто скрывают потенциальные уязвимости из-за сложности реализации. Для решения этой проблемы модель LiDO инновационно предлагает трехуровневую уточненную верификационную структуру:

1. Безопасный абстрактный уровень: отображение протокола в линеаризованную машину состояний, обеспечивающее консистентность журналов (безопасность);
2. Активный уровень гарантии: введение механизма "Pacemaker", который решает проблему задержки сети с помощью тайм-аутов и синхронизации раундов;
3. Расширенный уровень DAG: поддержка новых DAG-протоколов, таких как Narwhal и Bullshark, для эффективной проверки без лидеров консенсуса.

В настоящее время LiDO успешно применяется в промышленном протоколе Jolteon (двухфазный BFT) и нескольких DAG-протоколах, завершив механизированное доказательство более 10 000 строк кода Coq, из которых объем кода для проверки безопасности и активности составил соответственно 4 000 и 1 700 строк. Профессор Шао Чжун в своей речи подчеркнул: "В настоящее время протоколы консенсуса PoS в целом сталкиваются с проблемой, когда трудно одновременно обеспечить безопасность, активность и децентрализацию. Модель LiDO была предложена как системное решение для преодоления этой проблемы."

Профессор Шао Чжун и его команда ранее разработали CertiKOS, который является первой в мире операционной системой "без уязвимостей", прошедшей формальную проверку, и был назван "вехой в безопасности киберфизических систем". Это достижение не только закрепило их глубокие знания в области системной безопасности, но и продемонстрировало их профессиональные способности в этой области. В последние годы профессор Шао Чжун углубленно изучает безопасность блокчейна и в 2017 году совместно со своим студентом профессором Гу Жуньхуэем ввел технологии формальной проверки в область обеспечения безопасности смарт-контрактов и цепочных протоколов, обеспечивая безопасность криптоактивов на сумму в тысячи миллиардов долларов.

LiDO в настоящее время завершил проектирование модели и формальную проверку, и начал исследовать возможность интеграции с основными публичными цепочками и децентрализованными протоколами. Профессор Шао Чжун отметил, что они стремятся проверить ключевые механизмы в Web3.0, чтобы предоставить продукты и услуги на весь цикл, лучше поддерживая долгосрочные стратегии развития Web3 компаний и экосистем. В конце своей речи профессор Шао Чжун подчеркнул: "Достоверный, безопасный и проверяемый стек сетевых протоколов будет ключевым путем к истинно децентрализованному будущему."