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

ما يثير الاهتمام هنا هو التحول الذي يحدث في طريقة تفكير الناس حول الأمان. بدلاً من الاعتماد على الاختبارات التجريبية وتدقيقات الكود (النهج التقليدي)، هناك نموذج ناشئ حيث يتحقق المطورون من خصائص البرامج من خلال براهين قابلة للفحص بواسطة الآلة. إنه كأنك تنقل الأمان من "نعتقد أن هذا آمن" إلى "هذا لا يمكن أن يفشل بهذه الطرق بشكل برهاني". لقد بدأ النظام البيئي في تطبيق ذلك على البنى التحتية الحيوية—تنفيذات EVM، أنظمة إثبات STARK، التوقيعات المقاومة للكمبيوتر الكمومي، والبروتوكولات مثل إثباتات المعرفة الصفرية التي تدعم الكثير من الاتصالات المشفرة الحديثة.

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

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

الفرصة الحقيقية تكمن في تركيز جهود التحقق الرسمي على الأنظمة الحيوية—بروتوكولات البلوكتشين، نوى أنظمة التشغيل، والأشياء التي يمكن أن يؤدي فشلها إلى عواقب متسلسلة. هذا هو المكان الذي تحصل فيه على أكبر عائد من الجهد. الأمر لا يتعلق بإثبات كل شيء؛ بل بتعزيز البنية التحتية التي تعتمد عليها باقي الأنظمة بشكل استراتيجي.

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