يقوم Common Prefix بتأكيد رسمي لبروتوكول الإقراض في دفتر XRP لإثبات رياضي أنه لا يمكن تفريغه أو إفلاسه أو خرق قواعده. يركز العمل على بروتوكول الإقراض المقدم عبر XLS-66. وقد شرح Common Prefix منهجيته في سلسلة مكونة من ستة أجزاء، بما في ذلك سبب اختياره لـ Lean 4 في عملية التحقق. قال Common Prefix إن التحقق الرسمي يتجاوز اختبار البرمجيات العادي باستخدام الرياضيات لإثبات أن النظام يعمل بشكل صحيح في جميع الحالات الممكنة. وقال مُحقق دفتر XRP، فيت، المعروف أيضًا باسم حسين زنغانة، إن التحقق الرسمي يستخدم بالفعل في الأنظمة عالية المخاطر مثل التكنولوجيا العسكرية وبرمجيات حركة المرور الجوي وأنظمة التحكم في الطيران ومحطات الطاقة النووية. وأوضح أن هذا المنهج يستخدم الرياضيات لإظهار أن النظام يظل صالحًا عبر جميع المدخلات الممكنة، وليس فقط الحالات التي اختبرها المطورون. نظر Common Prefix في عدة أدوات، بما في ذلك Dafny وLean 4 وTLA+ وP. وقررت الفريق أن TLA+ وP غير مناسبين للأسئلة المحددة التي كان عليهم الإجابة عنها بشأن بروتوكول الإقراض. واحدة من الأسباب التي دفعتهم لاختيار Lean 4 هي أنه لا يعتمد على حلّال SMT. ووجد Common Prefix أن حلّال Dafny قد يتجاوز الوقت المسموح به أحيانًا عند التعامل مع الحسابات المعقدة المطلوبة للتحقق. يتطلب Lean مزيدًا من العمل يدويًا، لكن هذا يجعل من السهل على المطورين اكتشاف الأخطاء وإصلاحها. #Ripple https://t.co/s0YcQ4KAWX