На峰会上 Web3 впервые представлен модель 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, при этом количество кода для проверки безопасности и активности составило соответственно 4000 и 1700 строк. Профессор в своем выступлении подчеркнул: "В настоящее время протоколы консенсуса PoS в целом сталкиваются с трудностями в достижении безопасности, активности и децентрализации одновременно. Модель LiDO была предложена как системное решение для преодоления этого瓶颈."

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

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