Finite Field
فحص خلال 30 ثانيةغير متاح بعد

MPK Assurance / مراجعة جاهزية إثبات Go

نحن نثبت
كود Go لديك، ولا نكتفي باختباره.

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

جرّب عرض استرداد الأموال في 30 ثانية اطلب مراجعة جاهزية الإثبات
لأول 5 شركات فقط عرض التبني المبكر لـ MPK JPY 49,800(قبل الضريبة)
ابدأ بدالة Go واحدة
حتى خاصيتين
لا إدخال علني
لكود سري
تسليم
أدلة قابلة لإعادة الفحص

محلل MPK

مباشر
refund.go
func ApplyRefund(paid, refunded, amount int64) (int64, error) {
  if amount < 0 {
    return refunded, errors.New("negative amount")
  }
  if refunded+amount > paid {
    return refunded, errors.New("exceeds paid")
  }
  return refunded + amount, nil
}
الخاصية المطلوب التحقق منها

∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid

تم العثور على مثال مضاد

paid=100 و refunded=80 و amount=30 تنتهك الخاصية.

تحققت النواة

قبلت النواة الشهادة القياسية للنسخة المصححة.

تحقق يتجاوز الاختباراتابدأ من Go العاديافصل الذكاء الاصطناعي عن قرارات الثقةاعرض الإثبات والأمثلة المضادة والاستبعادات

عرض استرداد الأموال في 30 ثانية

اعثر على مثال مضاد، ثم أثبت النسخة المصححة.

جرّب كود استرداد الأموال المجهز وشاهد المسار من المثال المضاد إلى الإصلاح ثم الإثبات الناجح. لا تحتاج إلى إدخال كود سري في العرض العام.

سياسة الاسترداد: يجب ألا يتجاوز إجمالي المبالغ المستردة المبلغ المدفوع

الخاصية المطلوب التحقق منها

0 ≤ refunded + amount ≤ paid
  • الهدف: دالة واحدة لسياسة الاسترداد
  • المدخلات: أعداد صحيحة غير سالبة
  • الإدخال/الإخراج الخارجي وقاعدة البيانات والشبكة خارج النطاق
  • يُفحص ضمن افتراضات صريحة ومجموعة فرعية من Go

نتيجة التحقق (التنفيذ الذي يحتوي على خطأ)

تم العثور على مثال مضاد

وجدنا مدخلات ملموسة يتجاوز فيها إجمالي الاسترداد المبلغ المدفوع.

paid = 100
refunded = 80
amount = 30
result = 110 (انتهاك للخاصية)

التفاصيل التقنية

معرّف التشغيل
run_refund_bug_20260727
بصمة الشهادة
— لم تُنشأ لأن مثالًا مضادًا وُجد
حكم النواة
مرفوض / مثال مضاد
تقرير المسلمات
حساب الأعداد الصحيحة / افتراضات صريحة

تصنيف النتائج

أربعة أنواع للنتائج

تم الإثبات

الخاصية المحددة صحيحة ضمن الافتراضات والنطاق المعلنين.

مثبت
تم العثور على مثال مضاد

نعرض مدخلات ملموسة تنتهك الخاصية ونوضح الشرط الذي يحتاج إلى إصلاح.

مفند
غير محسوم

نوضح عندما لا تستطيع الاستراتيجية الحالية تحديد ما إذا كانت الخاصية صحيحة.

غير معروف
خارج النطاق

نشرح أسبابًا محددة لعدم إمكانية معالجة الهدف، مثل صياغة غير مدعومة أو إدخال/إخراج خارجي أو سلوك غير مدعوم.

غير قابل للتطبيق

الفرق عن الاختبار

نفحص الخاصية المحددة، لا مدخلات مختارة فقط.

الاختبار (قائم على الأمثلة)

  • يشغل الحالات التي كتبتها
  • يترك المدخلات غير المختارة بلا تغطية
  • نتيجة النجاح ليست شهادة
  • الثقة تعتمد على تصميم الاختبارات

MPK Assurance (إثبات)

  • يفحص الخصائص المحددة والنطاق
  • يعرض مدخلات ملموسة تكسر الخاصية
  • يترك شهادة وبصمة قابلتين لإعادة الفحص
  • النواة المستقلة تصدر الحكم النهائي
المقارنةالاختبارالإثبات
الهدفمدخلات مختارةخاصية محددة
عرض المثال المضاد△○
إعادة الفحصسجل التنفيذالشهادة
الحكم النهائيحزمة الاختباراتالنواة

3 مزايا

تحقق يتجاوز الاختبارات

نفحص الخاصية مقابل مواصفات وافتراضات ونطاق صريح، وليس مقابل عينات قليلة فقط.

استخدم Go، لا لغة إثبات خاصة

يمكنك البدء بدالة قواعد حرجة في Go ومعزولة عن الإدخال/الإخراج الخارجي.

دع الذكاء الاصطناعي يساعد في الإثبات، لكن لا تجعله مصدر الثقة

يعد الذكاء الاصطناعي المرشحات فقط. القبول النهائي تنفذه نواة مستقلة تقرأ الشهادة القياسية.

دع الذكاء الاصطناعي ينجز العمل، ولا تجعله يصدر الحكم النهائي.

العميليرسل دالة Go والخاصية المطلوب ضمانها
Geminiيقترح الخصائص والاستراتيجية ومرشحات الإثبات
MPKحد ثقة يفحص الشهادات باستقلالية
الإنسانيؤكد المواصفات والافتراضات والسرية
الأدلةيسلم حزمة أدلة قابلة لإعادة الفحص

يدير Gemini سير عمل الإثبات، وتتخذ MPK قرار الثقة، ويوافق الإنسان على التسليم.

حالات يساعد فيها التحقق

المبالغ المستردةيجب ألا يتجاوز إجمالي المبالغ المستردة المبلغ المدفوع
الرسوملا تكون سالبة ولا تتجاوز حدود العقد
الاحتياطياتلا ينخفض الرصيد بعد المعالجة عن الحد الأدنى
الخصوماتتبقى ضمن الحدود حتى عند تراكم الخصومات
النقاطلا تتجاوز النقاط الصادرة حد الميزانية
التوزيعمجموع المبالغ الموزعة يساوي أصل المبلغ

حزمة الأدلة

نسلم أدلة قابلة لإعادة الفحص، لا إجابة من الذكاء الاصطناعي.

شهادة MPK

مراجعة جاهزية الإثبات
سجل الشهادة القياسي

حكم النواة
مقبول
MPK
  • بصمة الشهادة
  • حكم نواة MPK
  • نتيجة فاحص Go المرجعي
  • تقرير المسلمات
  • الخصائص المثبتة والافتراضات المعلنة
  • النطاق المستبعد وأسباب الخروج عن النطاق
  • المثال المضاد، إن وجد
  • معرّف التشغيل ومعلومات إعادة الفحص

مراجعة جاهزية الإثبات

راجع أول دالة ضمن نطاق ثابت.

JPY 198,000 (قبل الضريبة)
  • دالة Go واحدة
  • حتى خاصيتين لإثباتهما
  • يصنف النتائج إلى مثبتة أو مثال مضاد أو غير محسومة أو خارج النطاق
  • حزمة أدلة وشرح مباشر للنتائج عبر الإنترنت
عرض تفاصيل التبني المبكر

هذا هو السعر القياسي المخطط. ندير حاليًا حملة تبن مبكر لأول 5 شركات فقط بسعر JPY 49,800 قبل الضريبة.

عرض التبني المبكر لـ MPK

لأول 5 شركات فقط

تحقق مما إذا كان كود Go الحرج لديك يمكن إثباته لا اختباره فقط.

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

ما الذي يشمله العرض

  • دالة Go واحدة
  • حتى خاصيتين لإثباتهما
  • تقييم التوافق مع MPK
  • تقرير عن الإثباتات والأمثلة المضادة ومعوقات الإثبات والعناصر الخارجة عن النطاق
  • تقرير يلخص نطاق الإثبات وافتراضاته

شروط الحملة

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

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

سير الخدمة

سير الخدمة (5 خطوات)

الاستكشاف

نؤكد سيناريو الفشل الذي قد يسبب خسارة والدالة المستهدفة.

تثبيت النطاق

نثبت الدالة والخاصية والافتراضات والنطاق المستبعد.

مراجعة Gemini + MPK

يجهز الذكاء الاصطناعي المرشحات، وتفحص MPK الشهادة.

شرح النتائج

نشرح الإثبات والمثال المضاد والنتيجة غير المحسومة والاستبعادات والأدلة.

الخطوات التالية

نوضح هل ينبغي الانتقال إلى الإصلاحات أو دوال إضافية أو تكامل CI/CD.

الأفضل ملاءمة

  • تنفذون منطق الاسترداد أو الرسوم أو الأرصدة في Go
  • خطأ واحد قد يسبب خسارة مالية أو عبئًا تدقيقيًا
  • لا تملكون فريق تحقق رسميًا مخصصًا
  • لديكم دالة صغيرة يمكن عزلها عن الإدخال/الإخراج الخارجي

القيود الحالية

  • إثبات تطبيق Go كامل غير محدد
  • معالجة شاملة تتضمن قاعدة بيانات أو واجهات API أو شبكة أو واجهة مستخدم
  • اكتشاف كل ثغرة أمنية
  • صياغة غير مدعومة أو اعتماديات خارجية أو مواصفات غير واضحة

الأسئلة الشائعة

أسئلة شائعة قبل الاستشارة الأولى

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

هل يزيل هذا كل الأخطاء؟

لا. نفحص الخاصية المحددة فقط ضمن الافتراضات والنطاق ومجموعة Go الفرعية المدعومة. هذا لا يضمن التطبيق الكامل أو الأنظمة الخارجية.

هل نحتاج إلى تعلم Lean أو Rocq؟

ليس للمراجعة الأولى. نبدأ بتأكيد دالة قواعد في Go معزولة عن الإدخال/الإخراج الخارجي والخاصية التي تريدون ضمانها.

هل يقرر الذكاء الاصطناعي ما هو الصحيح؟

لا. ينشئ Gemini الخصائص واستراتيجيات الإثبات ومرشحاته. نواة MPK المستقلة تقبل الشهادة النهائية أو ترفضها.

ماذا يحدث إذا فشل الإثبات؟

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

هل يمكن دمج ذلك في CI/CD؟

بعد أن تؤكد مراجعة جاهزية الإثبات الهدف وقابلية الإثبات، يمكننا تقديم اقتراح منفصل للفحوص المستمرة أو تكامل CI/CD.

هل نحتاج إلى إرسال الكود مع الاستفسار؟

لا تحتاجون إلى لصق كود سري في النموذج العام. بعد الاستفسار سنؤكد طريقة التعامل مع اتفاقية السرية وطريقة مشاركة آمنة.

اتصل بنا

تحقق مما إذا كان يمكن إثبات الكود لديك.

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

ندعم اتفاقية السرية ومشاركة الكود الآمنة

لا تدخل كود المصدر أو بيانات الاعتماد أو البيانات الشخصية في النموذج العام.

تم استلام معاينة الإرسال. في موقع الإنتاج، اربط ذلك بمسار الاستفسار الحالي.