في الأسبوع الماضي في OOPSALA '25 ، قدم مطورو Act لدينا نسخة محسنة وقابلة للتطوير من CheckMate ، وهي أداة آلية للتحقق رسميا من أمان نظرية اللعبة لبروتوكولات blockchain. باختصار: تتحقق الأداة مما إذا كانت الحوافز في البروتوكول تجعل الغش لا يستحق كل هذا العناء.

تحتاج البروتوكولات إلى 3 أنواع من الأمان: • التشفير: هل مفاتيحك / كلمات المرور قوية؟ • التنفيذ: هل توجد أخطاء في الكود؟ • نظرية اللعبة: هل الحوافز متوافقة بحيث لا يؤتي الغش ثماره؟ هذا الأخير أمر بالغ الأهمية ، ولكن غالبا ما يتم تجاهله.

يتعلق الأمن النظري لللعبة بالتأكد من أنه حتى الجهات الفاعلة العقلانية والأنانية تفضل اتباع القواعد - لأن الانحراف يكلف أكثر مما يكسب. إنه "اقتصاديات" الأمن.

يثبت CheckMate رسميا وتلقائيا أمان نظرية اللعبة باستخدام أدوات حل SMT. تقدم الورقة خوارزمية تركيبية "فرق تسد" تتوسع إلى ملايين العقد ، وإنشاء النماذج وتحليلها لتحقيق الكفاءة.

لماذا هذا مهم: يمكننا الآن إثبات أن حوافز بروتوكول blockchain تجعل الغش غير عقلاني - قبل النشر.