بالنسبة إلى كود Go الحرج، لا تكتف بالاختبارات.
بالنسبة إلى منطق Go الحرج الذي يحرّك الأموال، مثل المبالغ المستردة والرسوم والأرصدة والاحتياطيات، نفحص آليًا ما إذا كانت الخصائص المحددة صحيحة ضمن افتراضات ونطاق واضحين. ينشئ Gemini مرشحات الإثبات، ثم تصدر نواة MPK المستقلة الحكم النهائي.
المبالغ المستردة
الرسوم
الأرصدة
الاحتياطيات
الخصومات
التخصيصات
تحقق يتجاوز الاختبارات
افحص الخاصية المحددة على كامل النطاق المستهدف، لا على مدخلات مختارة فقط.
ابدأ من دالة Go واحدة
ابدأ بدالة قواعد حرجة، لا بلغة إثبات خاصة.
لا تثق بالذكاء الاصطناعي مباشرة
يحضّر الذكاء الاصطناعي المرشحات؛ أما القبول النهائي فيعود إلى النواة المستقلة.