قمة علماء Web3: قدم أستاذ ييل نموذج تحقق مبتكر لبروتوكول الإجماع
عُقد مؤتمر علماء Web3 لعام 2025 مؤخرًا، حيث ألقى البروفيسور شاو تشونغ من قسم علوم الكمبيوتر بجامعة ييل خطابًا رئيسيًا، كاشفًا للمرة الأولى عن نموذج LiDO وإطار LiDO-DAG الذي طوّره فريقه. تهدف هذه النتيجة الرائدة إلى تقديم إثباتات للأمان والنشاط القابلة للتطبيق الميكانيكي لبروتوكولات الإجماع المعقدة التي تتسم بالتحمل الخطأ البيزنطي (BFT)، لتأسيس قاعدة تقنية لتطوير موثوقية ونمو نظام Web3.
أشار البروفيسور شاو تشونغ في خطابه إلى أن بروتوكولات الإجماع الحالية تستخدم على نطاق واسع، لكنها غالبًا ما تخفي ثغرات محتملة بسبب تعقيد التنفيذ. لمعالجة هذه المشكلة، قدم نموذج LiDO إطار تحقق مفصل ثلاثي الطبقات بشكل مبتكر:
طبقة التجريد الآمنة: تحويل البروتوكول إلى آلة حالة خطية، لضمان اتساق السجلات (الأمان)；
طبقة ضمان النشاط: إدخال آلية "Pacemaker"، من خلال بث المهلة والتزامن بين الجولات لحل مشكلة تأخير الشبكة؛
طبقة التمديد DAG: تدعم بروتوكول DAG الناشئ، مما يحقق التحقق الفعال من الإجماع بدون قائد.
حالياً، تم تطبيق LiDO بنجاح على بروتوكولات المستوى الصناعي والعديد من بروتوكولات DAG، وأكمل أكثر من عشرة آلاف سطر من أكواد Coq لإثباتات ميكانيكية، حيث بلغ حجم كود التحقق من الأمان 4000 سطر وكود التحقق من النشاط 1700 سطر. أشار البروفيسور شاو تشونغ في خطابه إلى: "حالياً، تواجه بروتوكولات PoS للإجماع عمومًا تحديات في تحقيق الأمان والنشاط واللامركزية في نفس الوقت. إن نموذج LiDO هو الحل التصميمي المنهجي الذي تم طرحه لكسر هذه المعضلة."
البروفيسور شاو تشونغ يقود فريقه لتطوير CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" في العالم تم التحقق منه باستخدام طرق التحقق الشكلية، ويُعتبر "معلمًا في أمان الأنظمة الفيزيائية الشبكية". هذا الإنجاز لا يُرسّخ فقط الأساس التكنولوجي لشركته، بل يُبرز أيضًا تراكمه العميق في مجال أمان الأنظمة. في السنوات الأخيرة، تفرغ البروفيسور شاو تشونغ لأمان البلوكشين، وفي عام 2017، أسس شركة مع تلميذه البروفيسور غو رونغ هوي، حيث أدخل تقنية التحقق الشكلية إلى أمان العقود الذكية وبروتوكولات السلسلة، مما يضمن أمان الأصول المشفرة التي تبلغ قيمتها مئات المليارات.
لقد اكتمل تصميم نموذج LiDO والتحقق الرسمي منه، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية وبروتوكولات اللامركزية. أشار الأستاذ شاو تشونغ إلى أنهم ملتزمون بالتحقق من الآليات الأساسية في Web3.0 لتقديم منتجات وخدمات على مدى كامل الدورة، ودعم الاستراتيجيات الطويلة الأجل للشركات والبيئة في Web3 بشكل أفضل. في ختام حديثه، أكد الأستاذ شاو تشونغ: "ستكون البروتوكولات الشبكية الموثوقة والآمنة والقابلة للتحقق هي المسار الرئيسي نحو مستقبل لامركزي حقيقي."
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
أصدر أستاذ ييل نموذج LiDO لكسر صعوبة التحقق من بروتوكول الإجماع في Web3
قمة علماء Web3: قدم أستاذ ييل نموذج تحقق مبتكر لبروتوكول الإجماع
عُقد مؤتمر علماء Web3 لعام 2025 مؤخرًا، حيث ألقى البروفيسور شاو تشونغ من قسم علوم الكمبيوتر بجامعة ييل خطابًا رئيسيًا، كاشفًا للمرة الأولى عن نموذج LiDO وإطار LiDO-DAG الذي طوّره فريقه. تهدف هذه النتيجة الرائدة إلى تقديم إثباتات للأمان والنشاط القابلة للتطبيق الميكانيكي لبروتوكولات الإجماع المعقدة التي تتسم بالتحمل الخطأ البيزنطي (BFT)، لتأسيس قاعدة تقنية لتطوير موثوقية ونمو نظام Web3.
أشار البروفيسور شاو تشونغ في خطابه إلى أن بروتوكولات الإجماع الحالية تستخدم على نطاق واسع، لكنها غالبًا ما تخفي ثغرات محتملة بسبب تعقيد التنفيذ. لمعالجة هذه المشكلة، قدم نموذج LiDO إطار تحقق مفصل ثلاثي الطبقات بشكل مبتكر:
حالياً، تم تطبيق LiDO بنجاح على بروتوكولات المستوى الصناعي والعديد من بروتوكولات DAG، وأكمل أكثر من عشرة آلاف سطر من أكواد Coq لإثباتات ميكانيكية، حيث بلغ حجم كود التحقق من الأمان 4000 سطر وكود التحقق من النشاط 1700 سطر. أشار البروفيسور شاو تشونغ في خطابه إلى: "حالياً، تواجه بروتوكولات PoS للإجماع عمومًا تحديات في تحقيق الأمان والنشاط واللامركزية في نفس الوقت. إن نموذج LiDO هو الحل التصميمي المنهجي الذي تم طرحه لكسر هذه المعضلة."
البروفيسور شاو تشونغ يقود فريقه لتطوير CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" في العالم تم التحقق منه باستخدام طرق التحقق الشكلية، ويُعتبر "معلمًا في أمان الأنظمة الفيزيائية الشبكية". هذا الإنجاز لا يُرسّخ فقط الأساس التكنولوجي لشركته، بل يُبرز أيضًا تراكمه العميق في مجال أمان الأنظمة. في السنوات الأخيرة، تفرغ البروفيسور شاو تشونغ لأمان البلوكشين، وفي عام 2017، أسس شركة مع تلميذه البروفيسور غو رونغ هوي، حيث أدخل تقنية التحقق الشكلية إلى أمان العقود الذكية وبروتوكولات السلسلة، مما يضمن أمان الأصول المشفرة التي تبلغ قيمتها مئات المليارات.
لقد اكتمل تصميم نموذج LiDO والتحقق الرسمي منه، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية وبروتوكولات اللامركزية. أشار الأستاذ شاو تشونغ إلى أنهم ملتزمون بالتحقق من الآليات الأساسية في Web3.0 لتقديم منتجات وخدمات على مدى كامل الدورة، ودعم الاستراتيجيات الطويلة الأجل للشركات والبيئة في Web3 بشكل أفضل. في ختام حديثه، أكد الأستاذ شاو تشونغ: "ستكون البروتوكولات الشبكية الموثوقة والآمنة والقابلة للتحقق هي المسار الرئيسي نحو مستقبل لامركزي حقيقي."