Professor Shao Zhong, Co-Founder of CertiK, nimmt am Web3 Scholars Summit teil und präsentiert erstmals das LiDO-Modell.

Am 8. April hielt Shao Zhong, Professor am Department of Computer Science der Yale University und Mitbegründer von CertiK, auf der Web3 Scholars Conference 2025 in Hongkong eine Grundsatzrede 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 diesem Vortrag wies Professor Shao Zhong darauf hin, dass bestehende Konsensprotokolle (wie PBFT und Jolteon) zwar weit verbreitet sind, diese jedoch aufgrund ihrer komplexen Implementierung oft potenzielle Schwachstellen verbergen. Um dieses Problem zu lösen, schlägt das LiDO-Modell auf innovative Weise einen dreischichtigen detaillierten Verifikationsrahmen vor:

Sichere Abstraktionsschicht: Protokolle in eine linearisierte Zustandsmaschine abbilden, um die Konsistenz der Protokolle (Sicherheit) zu gewährleisten;

Aktive Sicherungsebene: Einführung des “Pacemaker”-Mechanismus, der durch Zeitüberschreitungs-Broadcast und Runden-Synchronisation das Problem der Netzwerkverzögerung löst;

DAG Erweiterungsschicht: Unterstützt aufstrebende DAG-Protokolle wie Narwhal und Bullshark und ermöglicht eine effiziente Validierung des konsenslosen Konsens.

Derzeit wurde LiDO erfolgreich in das industrielle Protokoll Jolteon (zwei-stufige BFT) und mehrere DAG-Protokolle integriert und hat die mechanisierte Beweisführung von über zehntausend Zeilen Coq-Code abgeschlossen, wobei die Sicherheits- und Aktivitätsvalidierung jeweils 4000 und 1700 Zeilen Code umfasst. “Aktuell sieht sich das PoS-Konsensprotokoll allgemein der Herausforderung gegenüber, Sicherheit, Aktivität und Dezentralisierung nicht gleichzeitig zu erreichen”, bemerkte Professor Zhao Zhong in seiner Rede. “Das LiDO-Modell ist genau das systematische Designkonzept, das vorgeschlagen wurde, um diese Herausforderung zu überwinden.”

Professor Shao Zhong und sein Team haben CertiKOS entwickelt, das weltweit erste “fehlerfreie” Betriebssystem, das durch formale Verifizierung validiert wurde und als “Meilenstein für die Sicherheit von cyber-physischen Systemen” gilt. Dieser Erfolg hat nicht nur die technische Basis des Sicherheitsunternehmens CertiK gelegt, sondern auch dessen tiefgreifende Ansammlung im Bereich der Systemsicherheit hervorgehoben. In den letzten Jahren hat Professor Shao Zhong intensiv an der Sicherheit von Blockchain gearbeitet und 2017 zusammen mit seinem Schüler Professor Gu Ronghui CertiK gegründet, um die formale Verifizierungstechnologie in die Sicherheitsgarantie von Smart Contracts und On-Chain-Protokollen einzuführen, und so die Sicherheit von Krypto-Assets 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 der Rede betonte Professor Shao Zhong: “Ein vertrauenswürdiger, sicherer und verifizierbarer Netzwerkprotokollstapel wird der Schlüsselweg zu einer wirklich dezentralisierten Zukunft sein.”