في قمة علماء Web3، أستاذ ييل يكشف عن نموذج LiDO لأول مرة

في قمة علماء Web3 لعام 2025، ألقى أستاذ قسم علوم الكمبيوتر في جامعة ييل، شاو جونغ، خطابًا بعنوان "إثبات أمان وفعالية بروتوكول الإجماع المعتمد على التكرير: LiDO وتوسيعه"، حيث كشف لأول مرة عن نموذج LiDO وإطار التوسع LiDO-DAG الذي طوره فريقه. تهدف هذه النتيجة الرائدة إلى توفير إثباتات قابلة للتحقق آليًا للأمان والفعالية لبروتوكولات الإجماع المعقدة المقاومة للبيزنطة (BFT)، مما يمهد الطريق لتطوير موثوق وذو نطاق واسع لبيئة Web3.

أشار الأستاذ شاو تشونغ إلى أن بروتوكولات التوافق الحالية تستخدم على نطاق واسع، لكنها تخفي عادةً ثغرات محتملة بسبب تعقيد التنفيذ. لحل هذه المشكلة، قدم نموذج LiDO إطار تحقق مفصل مبتكر من ثلاث طبقات:

1. طبقة التجريد الآمنة: تحويل البروتوكول إلى آلة حالة خطية، لضمان اتساق السجلات (الأمان)؛
2. طبقة حماية النشاط: إدخال آلية "Pacemaker"، من خلال البث المتأخر ومزامنة الجولات لحل مشكلة تأخير الشبكة؛
3. طبقة التوسع DAG: تدعم بروتوكولات DAG الناشئة، مما يحقق تحققًا فعالًا بدون قيادة.

حاليًا، تم تطبيق LiDO بنجاح على بروتوكول الصناعة Jolteon (BFT ذو مرحلتين) والعديد من بروتوكولات DAG، وتم الانتهاء من أكثر من عشرة آلاف سطر من كود Coq لإثبات الميكانيكي، حيث بلغ حجم كود التحقق من الأمان 4000 سطر والتحقق من النشاط 1700 سطر. أشار البروفيسور شاو تشونغ في حديثه إلى: "حاليًا، تواجه بروتوكولات إجماع PoS عمومًا صعوبة في تحقيق الثلاثة: الأمان، النشاط واللامركزية. نموذج LiDO هو بالضبط الحل التصميمي النظامي المقترح لكسر هذه المعضلة."

قام البروفيسور شاو تشونغ بقيادة فريقه لتطوير CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" في العالم يتم التحقق منه بشكل رسمي، ويُعتبر "معلمًا بارزًا في أمان أنظمة الشبكات الفيزيائية". لا يقتصر هذا الإنجاز على تأسيس أساس تقني له في مجال أمان الأنظمة، بل يُظهر أيضًا تراكمه العميق. في السنوات الأخيرة، قام البروفيسور شاو تشونغ بالغوص في أمان blockchain، وفي عام 2017، شارك مع تلميذه البروفيسور غو رونغ هوي لإدخال تقنية التحقق الرسمي إلى أمان العقود الذكية وبروتوكولات السلسلة، مما يوفر الأمان لأصول التشفير التي تصل قيمتها إلى مئات المليارات من الدولارات.

لقد أكملت LiDO حاليًا تصميم النموذج والتحقق الرسمي، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية والبروتوكولات اللامركزية. وأشار البروفيسور شاو تشونغ إلى أنهم ملتزمون بالتحقق من الآليات الرئيسية في Web3.0 لتقديم منتجات وخدمات شاملة، ودعم الاستراتيجيات طويلة الأجل لشركات Web3 والبيئة. وفي نهاية العرض، شدد البروفيسور شاو تشونغ على: "ستكون البروتوكولات الشبكية الموثوقة والآمنة والقابلة للتحقق هي المسار الرئيسي نحو مستقبل لامركزي حقيقي."