XRPL teste son protocole de prêt face à l’insolvabilité

Common Prefix vérifie formellement le Lending Protocol à venir de XRP Ledger avec Lean 4, afin de tester la validité de ses règles comptables et de sécurité dans les différents états possibles du système. Ce travail fait suite à la sortie de xrpld 3.4.0, qui inclut LendingProtocolV1_1, un amendement nécessitant encore l’approbation des validateurs avant son activation.

Le protocole repose sur des coffres de prêt à durée fermée. Les déposants peuvent ajouter ou retirer des actifs pendant la période de souscription, mais les capitaux sont bloqués pendant la période d’investissement et deviennent disponibles pour des prêts à durée fixe et non garantis. Les retraits reprennent pendant la période de remboursement. La comptabilité de caisse n’enregistre les intérêts qu’à la réception des paiements des emprunteurs, et non au moment de l’octroi des prêts.

Pourquoi c’est important

Des défaillances comptables dans les soldes des coffres, les paiements de prêts ou le calcul des parts pourraient affecter les fonds mis en commun par les déposants. Les travaux antérieurs de Common Prefix avaient révélé des violations d’invariants des coffres, des échecs d’assertions concernant les paiements de prêts, des erreurs d’arrondi arithmétique et des écarts entre les spécifications écrites et l’implémentation. RippleX a indiqué que ces problèmes avaient été corrigés dans les versions 3.1.3 et 3.2.0 de xrpld.

Le travail actuel recrée la logique pertinente du protocole dans Lean 4, plutôt que de tenter de vérifier l’intégralité du code C++ de xrpld. Un oracle compare des entrées équivalentes entre le modèle mathématique et l’implémentation de production, ce qui aide à repérer les divergences à mesure que le logiciel évolue.

Impact sur le marché

La vérification formelle peut renforcer la confiance dans l’infrastructure de prêt du XRPL avant l’activation de l’amendement par les validateurs et avant l’engagement de capitaux supplémentaires par les déposants. La conception suscite également l’intérêt commercial d’Evernorth et de VS1.Finance, ce qui accroît l’importance d’une comptabilité prévisible des coffres.

La portée de la preuve reste clairement limitée. Le remboursement des emprunteurs, la souscription des prêts et l’évaluation du crédit restent hors chaîne, tandis que le capital de première perte des courtiers n’élimine pas le risque de défaut. La vérification peut tester des propriétés et des hypothèses définies, mais elle ne peut pas prouver que chaque emprunteur, intégration externe ou processus opérationnel fonctionnera de manière sûre.