На саміті Web3 вперше публічно представлено модель LiDO, що пропонує нові підходи до безпеки консенсус протоколу

На нещодавній конференції Web3 Scholar Summit 2025 професор кафедри комп'ютерних наук Єльського університету виступив з доповіддю на тему «Безпека та активність доказів на основі уточненого протоколу консенсусу: LiDO та його розширення», вперше представивши громадськості модель LiDO та розширену архітектуру LiDO-DAG, розроблену його командою. Цей інноваційний результат покликаний забезпечити механізовану верифікацію безпеки та активності для складних протоколів консенсусу з баєзантинською помилкою (BFT), закладаючи технологічну основу для надійності та масштабування розвитку екосистеми Web3.

Цей професор у своїй доповіді зазначив, що незважаючи на те, що існуючі протоколи консенсусу (такі як PBFT, Jolteon) вже широко використовуються, їхня висока складність реалізації часто приховує потенційні вразливості безпеки. Для вирішення цієї проблеми модель LiDO інноваційно запропонувала трирівневу структуру уточненої перевірки:

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

Наразі LiDO успішно застосовується в промислових протоколах Jolteon (двоступеневий BFT) та в кількох DAG протоколах, було завершено понад десять тисяч рядків механізованого доказу коду Coq, з яких обсяг коду перевірки безпеки та активності становить відповідно 4000 рядків та 1700 рядків. Професор у своїй промові підкреслив: "На сьогодні протоколи консенсусу PoS загалом стикаються з труднощами досягнення безпеки, активності та децентралізації одночасно. Модель LiDO є системним дизайнерським рішенням, запропонованим для подолання цього вузького місця."

Варто зазначити, що цей професор раніше очолював команду, яка розробила першу у світі "безвідмовну" операційну систему CertiKOS через формальну верифікацію, що отримала визнання в галузі як "переломний момент у безпеці кіберфізичних систем". Це досягнення не лише заклало технологічну основу для безпечної компанії, яку він заснував пізніше, але й продемонструвало його глибокі знання в галузі системної безпеки. Останніми роками цей професор глибоко досліджує безпеку блокчейну, впроваджуючи технологію формальної верифікації в область забезпечення безпеки смарт-контрактів та протоколів на ланцюгу, забезпечуючи безпеку криптоактивів на ринку в тисячах мільярдів доларів.

Модель LiDO наразі завершила розробку та формальну верифікацію, і почала досліджувати можливості інтеграції з основними публічними блокчейнами та децентралізованими протоколами. Цей професор зазначив, що вони прагнуть верифікувати ключові механізми в Web3.0, щоб забезпечити продукти та послуги на всьому протязі циклу, краще підтримуючи стратегію довгострокового розвитку Web3 компаній та екосистеми. Наприкінці виступу він підкреслив: "Достовірний, безпечний, перевіряємий стек мережевих протоколів стане ключовим шляхом до справжнього децентралізованого майбутнього."