XRPL kredi protokolünde Lean 4 ile biçimsel doğrulama başladı

XRP Ledger’ın (XRPL) yeni kredi protokolü, fon akışlarıyla muhasebe kurallarını ihlal edip etmediğinin matematiksel olarak doğrulanması sürecine girdi. Ancak bu doğrulama, borçluların temerrüt veya kredi riskini ortadan kaldırmıyor.

Protokol araştırma şirketi Common Prefix, 17 Eylül’de XRPL kredi protokolünü, teorem ispatlama dili Lean 4 kullanarak biçimsel olarak doğruladığını açıkladı. Doğrulamanın kapsamını mevduat, kredi, geri ödeme ve itfa süreçlerinin belirlenen muhasebe ve güvenlik kurallarını ihlal edip etmediği oluşturuyor.

Biçimsel doğrulama, belirli senaryoları çalıştıran standart testlerden farklı. Araştırmacılar, xrpld C++ kodunun tamamını doğrudan kanıtlamak yerine temel mantığı Lean 4 modeliyle yeniden oluşturuyor ve modelin karşılaması gereken özellikleri tanımlıyor.

Daha sonra modele ve gerçek uygulamaya aynı girdiler uygulanarak sonuçların eşleşip eşleşmediği kontrol ediliyor. Bu nedenle kanıtın kapsamı, modele dahil edilen durumlar ve araştırmacıların belirlediği varsayımlarla sınırlı kalıyor. Common Prefix, kamuya açık materyallerinde tek varlıklı kasayla kredi protokolüne yönelik resmi doğrulama çalışmalarını açıklıyor.

Bu çalışma, XRPL kredi işlevinin ana ağda tamamen etkinleştirildiği anlamına gelmiyor. Ripple’ın açık kaynak belgeleri, LendingProtocolV1_1’i kapalı kasalar ve nakit esaslı muhasebe getiren bir amendment olarak tanımlıyor. Gerçek uygulama için ana ağ oylaması ve mutabakat sürecinin tamamlanması gerekiyor.

XRPLF’nin yayımladığı xrpld 3.4.0 sürüm kayıtlarında LendingProtocolV1_1 ile ilgili işlevler yer alıyor. Ancak bir işlevin koda eklenmesiyle ilgili amendment’ın defterde etkinleştirilmesi birbirinden ayrı süreçler.

LendingProtocolV1_1 kapsamındaki kasalar abonelik, yatırım ve itfa olmak üzere üç aşamada çalışıyor. Abonelik aşamasında fon yatırma ve çekme işlemleri yapılabilirken yatırım aşamasında fonlar kilitlenerek yeni kredilerde kullanılıyor. Kredi vadesine ulaşıp geri ödendiğinde yatırımcılar itfa aşamasında paylarını nakde çevirebiliyor.

XRPL’nin resmi tek varlıklı kasa belgesi, aşamalara göre işlem koşullarını ortaya koyuyor. Bu yapı, mevduatların ne zaman krediye aktarılacağını ve ne zaman itfa edilebileceğini defter durumuna yansıtıyor.

Muhasebe yöntemi de değişiyor. Mevcut yapıda kredi kullandırıldığı anda gelecekteki faiz gelir olarak kaydedilirken LendingProtocolV1_1, faizi gerçek geri ödeme alındığında kaydeden nakit esaslı muhasebe yöntemini kullanıyor.

Bu yöntem, tahsil edilmemiş faizin kasa varlıklarına ve pay değerine önceden yansıtılması sorununu azaltmayı amaçlıyor. Ancak muhasebe kuralları daha ayrıntılı hale gelse bile borçlunun geri ödeme yapmaması riski ortadan kalkmıyor.

Önceki doğrulama süreçlerinde kasa değişmezlerinin ihlali, kredi geri ödeme doğrulama hataları, aritmetik yuvarlama sorunları ve XLS spesifikasyonuyla gerçek uygulama arasındaki farklar tespit edildi. RippleX, ilgili düzeltmelerin xrpld 3.1.3 ve 3.2.0 sürümlerine eklendiğini geliştirici paylaşımında belirtti.

Bu bulgular, biçimsel doğrulamanın yalnızca lansman öncesi bir kontrol olmadığını, uygulama ile spesifikasyon arasındaki farkları tespit etmek için de kullanılabileceğini gösteriyor. Buna karşılık doğrulama modeline dahil edilmeyen durumlar veya araştırmacıların belirlemediği varsayımlar kanıt kapsamına girmiyor.

XRPL kredi protokolünün kredi riski ise ayrı bir konu olarak kalıyor. XRPL kredi protokolü belgeleri, teminat ve otomatik tasfiye yerine borçluların kredi değerlendirmesi ile kredi tahsis incelemesinin zincir dışında yapılacağını belirtiyor.

Kredi brokerlarının sağladığı kıdemli zarar üstlenme sermayesi bazı kayıpları karşılayabilir, ancak borçlunun temerrüdünü ortadan kaldırmaz. Bu nedenle mevcut doğrulama, borçlunun mutlaka geri ödeme yapacağını değil, defter içindeki mevduat, kredi, geri ödeme ve itfa muhasebesinin tanımlanan kurallara göre çalışıp çalışmadığını inceliyor.

XRPL’nin kurumsal kredi altyapısına ilişkin tartışmalar daha önce TokenPost tarafından da ele alınmıştı. Mevcut biçimsel doğrulama, bu tür kredi işlevlerinin gerçek deftere uygulanmasından önce muhasebe ve durum geçişlerinin istikrarını değerlendirme aşaması niteliğinde.

Ana ağda etkinleştirme durumu ve nihai doğrulama kapsamı kesinleşmeden XRPL kredi piyasasının güvenliğinin kanıtlandığını söylemek mümkün değil. Önümüzdeki dönemde LendingProtocolV1_1 amendment’ının onaylanıp onaylanmadığı ve zincir dışı kredi inceleme yapısının nasıl işleyeceği izlenecek.