فيتاليك: من المتوقع أن يعزز التحقق الشكلي المدعوم بالذكاء الاصطناعي كفاءة وأمان الكود في آن واحد

أفادت Foresight News أن Vitalik Buterin نشر مقالاً يناقش آفاق تطبيق التحقق الشكلي في مجال أمن البلوكشين. تشير المقالة إلى أن هناك نموذجاً جديداً ناشئاً في مجال البحث والتطوير المتقدم في Ethereum، حيث يتم كتابة الشيفرة مباشرة باستخدام EVM bytecode أو Assembly أو Lean، والتحقق من صحتها من خلال البراهين الرياضية القابلة للفحص التلقائي في Lean. وقد أطلق الباحث Yoichi Hirai على هذا النموذج اسم "الشكل النهائي لتطوير البرمجيات". يرى Vitalik أن التحقق الشكلي المدعوم بالذكاء الاصطناعي قد يعزز كفاءة وأمان الشيفرة في الوقت ذاته، وهو مناسب بشكل خاص لوحدات الأمان الأساسية مثل STARK وZK-EVM وتوقيعات مقاومة الحوسبة الكمية وخوارزميات الإجماع. كما تؤكد المقالة أن التحقق الشكلي ليس حلاً شاملاً، إذ قد يفشل بسبب النطاق غير الكامل للإثبات، أو أخطاء المواصفات، أو القنوات الجانبية المتعلقة بالأجهزة. وفي المستقبل، قد تنقسم البرمجيات إلى "نواة أمان" و"هامش غير آمن"، مع كون Ethereum واحدة من أهم نوى الأمان.