Common Prefix, $XRP Ledger Kredi Protokolü'nün matematiksel olarak boşaltılamayacağını, iflas edemeyeceğini veya kurallarını çiğneyemeyeceğini kanıtlamak için resmi doğrulama sürecini yürütüyor. Çalışma, XLS-66 aracılığıyla tanıtılan Kredi Protokolüne odaklanıyor. Common Prefix, doğrulama sürecinde Lean 4'ü neden seçtiğini de içeren altı bölümlük bir dizi makalede yaklaşımını açıkladı. Common Prefix, resmi doğrulamanın, sistemin tüm olası durumlarda doğru çalıştığını matematiksel olarak kanıtlayarak normal yazılım testlerinin ötesine geçtiğini belirtti. XRP Ledger doğrulayıcısı Vet, diğer adıyla Hussein Zangana, resmi doğrulamanın askeri teknoloji, hava trafiği yazılımı, uçuş kontrol sistemleri ve nükleer santraller gibi yüksek riskli sistemlerde zaten kullanıldığını söyledi. O, bu yaklaşımın, geliştiricilerin test ettiği durumlar değil, tüm olası girdiler boyunca sistemin geçerliliğini matematiksel olarak gösterdiğini açıkladı. Common Prefix, Dafny, Lean 4, TLA+ ve P gibi birkaç araç üzerinde çalıştı. Takım, TLA+ ve P'nin kredi protokolüyle ilgili cevaplamak zorunda kaldığı özel sorular için uygun olmadığını kararlaştırdı. Lean 4'ü seçme nedenlerinden biri, SMT çözücüye bağımlı olmamasıdır. Common Prefix, Dafny'nin çözücüsünün doğrulama için gerekli olan karmaşık aritmetik işlemlerle başa çıkarken zaman aşımına uğrayabileceğini fark etti. Lean, el ile daha fazla çalışma gerektirir, ancak bu aynı zamanda hataların geliştiriciler tarafından daha kolay bulunup düzeltilmesini sağlar. #Ripple https://t.co/s0YcQ4KAWX