Los desarrolladores de XRP Ledger (XRPL) están sometiendo su próximo mercado de préstamos a una verificación matemática para comprobar si el protocolo puede llegar a vaciarse o volverse insolvente bajo alguno de los estados previstos por su diseño. El trabajo busca demostrar que las reglas contables y de seguridad se mantienen cuando se reciben depósitos, se conceden préstamos, llegan los pagos o se producen impagos.
Common Prefix, una firma especializada en investigación de protocolos, anunció el 17 de septiembre que está verificando formalmente el protocolo de préstamos de XRPL mediante Lean 4, un lenguaje diseñado para demostrar que un sistema cumple determinadas propiedades matemáticas. El objetivo no es revisar todo el código de xrpld, escrito en C++, sino reconstruir en Lean 4 la lógica relevante del protocolo y comprobar cómo se comporta en los distintos estados posibles.
Un sistema con capital bloqueado durante un periodo definido
La importancia de este análisis ha aumentado tras la publicación de la versión 3.4.0 de xrpld, que incorpora LendingProtocolV1_1. Esta actualización introduce bóvedas de préstamos cerradas y un sistema de contabilidad basado en caja. El código ya está incluido en el software de los servidores, pero la modificación todavía necesita ser aprobada mediante el proceso de enmiendas de XRP Ledger para entrar en vigor.
El diseño permite que los depositantes agrupen sus activos mientras los intermediarios de préstamos los destinan a operaciones de plazo fijo y sin garantía. La evaluación de los prestatarios y el análisis de su solvencia se realizan fuera de la cadena. El libro mayor registra la creación de los préstamos, los reembolsos y la contabilidad asociada.
Las bóvedas cerradas atraviesan tres fases: suscripción, inversión y reembolso. Durante la primera, los usuarios pueden añadir o retirar activos. Cuando comienza la fase de inversión, ambas operaciones quedan suspendidas y el capital pasa a estar disponible para conceder préstamos. Las retiradas se reanudan al llegar la fase de reembolso. El calendario se fija al crear la bóveda y no puede modificarse después, de modo que los participantes conocen de antemano cuánto tiempo podría quedar comprometido su capital.
La nueva contabilidad basada en caja también modifica el momento en que se reconoce el interés. En el diseño anterior, los intereses previstos podían contabilizarse como ingresos cuando se originaba el préstamo, aunque el prestatario aún no los hubiera pagado. Con el nuevo sistema, solo se reconocen cuando se reciben, lo que reduce el riesgo de que el valor de las participaciones de la bóveda incluya ingresos todavía pendientes.
La verificación ya detectó fallos en versiones anteriores
La iniciativa no parte de cero. Durante una fase exploratoria desarrollada entre febrero y abril, Common Prefix modeló partes del protocolo y definió las condiciones que debían conservarse. Según RippleX, ese trabajo detectó incumplimientos de las reglas internas de las bóvedas, fallos en comprobaciones vinculadas a los pagos, errores de redondeo y discrepancias entre las especificaciones escritas y su implementación.
Los problemas identificados se corrigieron posteriormente en las versiones 3.1.3 y 3.2.0 de xrpld. En la nueva fase, un mecanismo de comparación ejecuta entradas equivalentes contra el modelo matemático y contra la implementación utilizada en producción. Así puede señalar comportamientos distintos entre ambos.
La prueba, sin embargo, tiene un alcance concreto. Sus conclusiones dependen de las propiedades definidas por los investigadores y de las hipótesis incorporadas al modelo. Además, el protocolo de préstamos debe convivir con funciones ya existentes de XRPL, como las transferencias de activos, los bloqueos y las recuperaciones de fondos. Cada interacción amplía el número de estados que deben analizarse.
La solvencia de los prestatarios queda fuera del modelo
Incluso una verificación satisfactoria no eliminaría el riesgo de crédito. El protocolo depende de evaluaciones fuera de la cadena y no utiliza actualmente mecanismos automatizados de garantías y liquidaciones como los habituales en otros mercados de préstamos descentralizados. Los intermediarios pueden aportar capital de primera pérdida para absorber parte de un impago antes de que las pérdidas alcancen a los depositantes, pero la propia documentación de XRPL advierte de que esa estructura no elimina el riesgo.
La verificación tampoco puede demostrar que todas las integraciones externas, decisiones operativas o evaluaciones de crédito funcionarán correctamente. Su aportación se concentra en la primera capa de seguridad: que la contabilidad de XRPL sea coherente entre depósitos, préstamos, pagos y retiradas. La segunda seguirá dependiendo de cómo los intermediarios valoren y gestionen a los prestatarios.
RippleX ha señalado a Evernorth, que prepara su conversión en una compañía de tesorería de XRP cotizada en Nasdaq, y a VS1.Finance entre las empresas que preparan usos o desarrollos sobre las bóvedas de activo único y el protocolo de préstamos. Antes de que el sistema se active, los validadores tendrán que decidir sobre la enmienda. Los desarrolladores buscan llegar a ese momento con más evidencias de que la maquinaria contable se comporta como está especificado.
