NEAR AI تُحرز تقدّمًا في التحقّق الشكلي من العقود الأساسية

تعمل NEAR AI على جعل التحقق الصوري أكثر سهولة، مع التركيز في البداية على NEAR Protocol وعقوده الذكية الأساسية. يستخدم التحقق الصوري براهين رياضية للتأكد من أن البرمجيات تستوفي قواعد محددة؛ وهو يكمّل الاختبارات ومراجعة الشيفرة، لكنه لا يضمن الأمان الكامل. ينطلق هذا الجهد من تصدّر NEAR AI، بحسب ما أفادت به، ترتيب Lean Eval v1 من حيث إجمالي المسائل المحلولة. وعلى PutnamBench، حلّ نظامها 672 مسألة باستخدام Lean. وبلغت التكلفة المُعلنة نحو 0.17 دولار للمسألة، بينما يسجل المستودع تكاليف النماذج للتقديم بقيمة 111.85 دولارًا. وتحذّر NEAR من أن نتائج الاختبارات المعيارية لا تعكس التكلفة أو الجهد الكاملين اللازمين للتحقق من برمجيات الإنتاج. ولا يزال تطبيق التحقق الصوري على العقود المنشورة يتطلب نماذج دقيقة، وخصائص محددة بوضوح، وبراهين تتوافق مع التنفيذ. ولا تشمل الضمانات سوى الخصائص والافتراضات التي جرى التحقق منها؛ لذلك ينبغي أن يعمل التحقق الصوري إلى جانب الاختبارات ومراجعة الشيفرة والأمن التشغيلي. وتعكس المبادرة اهتمامًا أوسع بالبراهين المدعومة بالذكاء الاصطناعي، بما في ذلك أعمال ناقشتها Aptos Labs والمؤسس المشارك لإيثريوم Vitalik Buterin. وبالنسبة لمتداولي NEAR، فهذا تطور أمني محتمل على المدى الطويل، وليس إعلانًا عن إطلاق أو محفزًا فوريًا للرمز.