На саміті веб3 професор Єльського університету вперше публічно представив модель LiDO

На нещодавньому саміті Web3 вчених 2025 року професор комп'ютерних наук Єльського університету Шао Чжун виступив з доповіддю на тему «Безпека та активність доказів на основі уточнених консенсусних протоколів: 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 компаній та екосистеми. Наприкінці своєї промови професор Шао Чжун підкреслив: "Достовірний, безпечний, перевіряємий стек мережевих протоколів стане ключовим шляхом до справжнього децентралізованого майбутнього."