Prof. Shao Zhong, Mitgründer von CertiK, nahm an der Web3 Akademiker-Konferenz teil und stellte erstmals das LiDO-Modell vor.

Auf der heute abgehaltenen Web3 Scholars Conference 2025 hielt Shao Zhong, Professor am Department of Computer Science der Yale University und Mitbegründer von CertiK, eine Keynote mit dem Titel “Proof of Security and Activity of Consensus Protocols Based on Refinement: LiDO and Its Extensions”, in der er das von seinem Team entwickelte LiDO-Modell und das LiDO-DAG-Erweiterungsframework erstmals vorstellte. Diese bahnbrechende Errungenschaft zielt darauf ab, einen mechanisch überprüfbaren Beweis für die Sicherheit und Lebendigkeit des komplexen Konsensprotokolls Byzantine Fault Tolerance (BFT) zu erbringen und damit eine technische Grundlage für die Zuverlässigkeit und groß angelegte Entwicklung des Web3-Ökosystems zu schaffen.

In seiner Rede wies Professor Shao Zhong darauf hin, dass bestehende Konsensprotokolle (wie PBFT, Jolteon) zwar weit verbreitet sind, jedoch aufgrund ihrer komplexen Implementierung potenzielle Schwachstellen verbergen. Um dieses Problem zu lösen, schlägt das LiDO-Modell innovativ einen dreischichtigen Verifizierungsrahmen vor:

• Sicherheitsabstraktionsschicht: Protokolle werden als linearisiertes Zustandsmaschinen abgebildet, um die Konsistenz der Protokolle (Sicherheit) zu gewährleisten;
• Aktivitätsgarantieebene: Einführung des “Pacemaker”-Mechanismus, um das Problem der Netzwerkverzögerung durch Timeout-Broadcast und Runden-Synchronisation zu lösen;
• DAG-Erweiterungsebene: Unterstützt aufstrebende DAG-Protokolle wie Narwhal und Bullshark und ermöglicht eine effiziente Validierung ohne führende Konsensfindung.

Derzeit wurde LiDO erfolgreich in dem industriellen Protokoll Jolteon (Zwei-Phasen-BFT) und mehreren DAG-Protokollen angewendet und hat die mechanische Beweisführung von über zehntausend Zeilen Coq-Code abgeschlossen, wobei die Code-Mengen für Sicherheits- und Aktivitätsvalidierung jeweils 4000 Zeilen und 1700 Zeilen erreichen. “Aktuell sieht sich das PoS-Konsensprotokoll allgemein dem Dilemma gegenüber, Sicherheit, Aktivität und Dezentralisierung nicht gleichzeitig zu erreichen,” wies Professor Shao Zhong in seinem Vortrag hin. “Das LiDO-Modell ist genau als systematischer Entwurf vorgeschlagen worden, um dieses Dilemma zu durchbrechen.”

Professor Shao Zhong und sein Team haben CertiKOS entwickelt, das weltweit erste “fehlerfreie” Betriebssystem, das durch formale Verifikation validiert wurde, und wird als “Meilenstein der Sicherheit von cyber-physikalischen Systemen” gefeiert. Dieser Erfolg legt nicht nur das technische Fundament des Sicherheitsunternehmens CertiK, sondern zeigt auch seine tiefen Kenntnisse im Bereich der Systemsicherheit. In den letzten Jahren hat Professor Shao Zhong intensiv an der Sicherheit von Blockchain gearbeitet und im Jahr 2017 zusammen mit seinem Schüler Professor Gu Ronghui CertiK gegründet, um formale Verifikationstechniken in die Sicherheitsgarantie von Smart Contracts und On-Chain-Protokollen einzuführen und die Sicherheit von Krypto-Vermögenswerten im Wert von mehreren Milliarden Dollar zu gewährleisten.

LiDO hat derzeit das Modell-Design und die formale Verifizierung abgeschlossen und beginnt, die Integrationsmöglichkeiten mit gängigen öffentlichen Blockchains und dezentralen Protokollen zu erkunden. Professor Shao Zhong erklärte, dass CertiK sich der Verifizierung der Schlüsselmechanismen im Web3.0 widmet, um Produkte und Dienstleistungen über den gesamten Lebenszyklus anzubieten und die langfristige Entwicklungsstrategie von Web3-Unternehmen und -Ökosystemen besser zu unterstützen. Am Ende seiner Rede betonte Professor Shao Zhong: “Ein vertrauenswürdiger, sicherer und verifizierbarer Netzwerkprotokollstack wird der Schlüsselweg zu einer wirklich dezentralisierten Zukunft sein.”