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

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