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

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

Професор Шао Чжун вказав, що існуючі консенсусні протоколи, хоча й широко використовуються, але через складність реалізації часто приховують потенційні вразливості. Щоб вирішити цю проблему, модель LiDO інноваційно пропонує трирівневу уточнену верифікаційну рамку:

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

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

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

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