ألقى مؤسس مشارك إيثيريوم فيتاليك بوتيرين في 18 مايو تحليلًا عميقًا استكشف فيه واقع وآفاق تقنيات التحقق الصوري (Formal Verification)، واعتبر أن التحقق الصوري بمساعدة الذكاء الاصطناعي سيصبح «الشكل النهائي لتطوير البرمجيات»، مشيرًا كذلك إلى أن إيثيريوم سيُشكّل جزءًا مهمًا من بنية «النواة الآمنة» في المستقبل.
المبدأ الجوهري للتحقق الصوري ومجالات التطبيق
بحسب تأكيد مقال فيتاليك، يُعدّ التحقق الصوري مناسبًا بشكل خاص للسيناريوهات التي تكون فيها «الأهداف أبعد من أن تكون أسهل من مجرد تحقيقها»، وقد سرد بوضوح أربعة مكونات تقنية محورية ضمن ترقية إيثيريوم للمرحلة التالية:
التوقيعات المقاومة للتهديدات الكمّية: أعمال تحقق صوري موجودة لتعددات توقيع SPHINCS
نظام الإثباتات STARK: مشروع Arkliib مكرّس لإنشاء تنفيذ STARK خاضع للتحقق الصوري بالكامل
خوارزميات توافقية لتحمّل الأخطاء البيزنطية: يجري العمل حاليًا على تحديد واثبات الخصائص الأمنية لتوافق Lean
ZK-EVM: مشروع evm-asm يهدف إلى إنشاء تنفيذ EVM كامل للتحقق الصوري (يستخدم مباشرة لغة تجميع RISC-V)
استشهد فيتاليك بقول يوشي هيراي، واصفًا هذا النهج بأنه «الشكل النهائي لتطوير البرمجيات».
اتجاه تطور بنية «النواة الآمنة» كما يصفها فيتاليك
بحسب تأكيد مقال فيتاليك، يصف نمط تطور بنى البرمجيات المستقبلية:
النواة الآمنة: تعزيز مستمر عبر الأساليب الصورية، لتحمل أعلى مستوى من الثقة؛ ويُصرّح فيتاليك بأن إيثيريوم ونواة نظام التشغيل وتطبيقات إنترنت الأشياء ذات الصلة ستصبح نواة آمنة.
الحافة غير الآمنة: تعمل المكونات الطرفية في بيئة حظر (sandbox)، مع منحها أقل الصلاحيات اللازمة لإنجاز العمل؛ وإذا تعطل المكون الطرفي، توفر النواة الآمنة الحماية.
قيود التحقق الصوري وأنماط الفشل
يعترف فيتاليك بأن التحقق الصوري ليس «سحرًا»؛ مستشهدًا بأعمال باحثين مثل Nadim Kobeissi (Cryspen)، حيث يؤكد ثلاث فئات رئيسية من أنماط الفشل: إغفال جزء من التحقق (يتم التحقق من جزء من الكود فقط بينما توجد عيوب جوهرية في الأجزاء غير المُتحقق منها)؛ إغفال في المتطلبات (خطأ في مواصفة الأمن نفسها أو احتواء البرهان على افتراضات خاطئة)؛ هجمات القنوات الجانبية (هجمات القنوات الجانبية على الحدود بين البرمجيات والأجهزة صعبة أن تلتقطها النماذج الحالية).
يؤكد فيتاليك أن «الصحة القابلة للإثبات» تتحقق جوهريًا من الاتساق الداخلي بين نوايا/تعبيرات مختلفة، وليس من التطابق المطلق مع نوايا البشر الحقيقية.
أدوات التحقق الصوري بمساعدة الذكاء الاصطناعي
بحسب تأكيد مقال فيتاليك على الأدوات المتاحة: Lean (لغة إثبات رياضية يمكنها التحقق آليًا من النظريات)؛ Claude وDeepseek 4 Pro (يؤكد فيتاليك أنهما كافيان للاستخدام في كتابة براهين Lean)؛ Leanstral (نموذج ترجيح مفتوح الأوزان بحجم 11.9 مليار معلمات، مُخصص لعمل ضبط دقيق لكتابة Lean، ويمكن تشغيله محليًا، ويُظهر أداءً في الاختبارات القياسية أفضل من كثير من النماذج العامة الأكبر حجمًا).
الأسئلة الشائعة
لماذا يعتقد فيتاليك أن على إيثيريوم أن يصبح «نواة آمنة»؟
بحسب مقال فيتاليك، يشبه إيثيريوم نواة نظام التشغيل من حيث أنه يتحمل أعلى مستوى من الثقة في عملية رقمنة المجتمع. ويشير إلى أن هدف تصميم النواة الآمنة يتمثل في الوصول بأمانها إلى معيار لا يسمح بتفشي أخطاء البرمجيات، وأن توجيه كل قدرات الحوسبة الإضافية التي يجلبها الذكاء الاصطناعي يكون للاستثمار في تعزيز أمن النواة الآمنة.
لماذا يُعدّ التحقق الصوري مناسبًا بشكل خاص لتقنيات STARK وZK-EVM وغيرها؟
بحسب تحليل فيتاليك، فإن السمة المشتركة لهذه التقنيات هي أن «الهدف أبعد بكثير من أن يكون أسهل من تحقيقه»؛ إذ يمكن تعريف خصائصها الأمنية بوضوح باستخدام لغة رياضية، لكن التنفيذ الفعلي معقّد جدًا، وهذا تحديدًا هو السيناريو الذي يبرز فيه التحقق الصوري أفضل ما يكون.
كيف ينصح فيتاليك المطورين باستخدام التحقق الصوري بمساعدة الذكاء الاصطناعي عمليًا؟
بحسب مقال فيتاليك، ينصح بأن يكتب الذكاء الاصطناعي كود Lean والبراهين الرياضية، بحيث يحتاج المستخدم في النهاية فقط إلى التحقق مما إذا كانت الجمل المُبرهنة تتوافق مع التوقعات، دون الاضطرار إلى كتابة أكواد البراهين التفصيلية الأساسية بنفسه. ويؤكد أن Claude وDeepseek 4 Pro وLeanstral هي الأدوات الرئيسية المتاحة حاليًا.
إخلاء المسؤولية: قد تكون المعلومات الواردة في هذه الصفحة مستمدة من مصادر خارجية وهي للمرجعية فقط. لا تمثل هذه المعلومات آراء أو وجهات نظر Gate ولا تشكل أي نصيحة مالية أو استثمارية أو قانونية. ينطوي تداول الأصول الافتراضية على مخاطر عالية. يرجى عدم الاعتماد حصرياً على المعلومات الواردة في هذه الصفحة عند اتخاذ القرارات. لمزيد من التفاصيل، يرجى الرجوع على
إخلاء المسؤولية.
