XRPL prueba su protocolo de préstamos contra la insolvencia

Common Prefix está verificando formalmente el próximo Lending Protocol de XRP Ledger con Lean 4, comprobando si sus reglas contables y de seguridad se mantienen en todos los posibles estados del sistema. El trabajo sigue a la publicación de xrpld 3.4.0, que incluye LendingProtocolV1_1, una enmienda que aún necesita la aprobación de los validadores antes de su activación.

El protocolo se articula en torno a bóvedas de préstamos de tipo cerrado. Los depositantes pueden aportar o retirar activos durante la suscripción, pero el capital queda bloqueado durante el periodo de inversión y queda disponible para préstamos sin garantía a plazo fijo. Los retiros se reanudan durante el reembolso. La contabilidad de caja registra los intereses solo cuando llegan los pagos del prestatario, y no en el momento de originar los préstamos.

Por qué importa

Los fallos contables en los saldos de las bóvedas, los pagos de préstamos o el cálculo de participaciones podrían afectar a los fondos agrupados de los depositantes. El modelado previo de Common Prefix descubrió violaciones de invariantes en las bóvedas, fallos de aserciones en los pagos de préstamos, errores de redondeo aritmético y diferencias entre las especificaciones escritas y la implementación. RippleX afirmó que esos problemas se resolvieron en las versiones 3.1.3 y 3.2.0 de xrpld.

El trabajo actual recrea la lógica relevante del protocolo en Lean 4, en lugar de intentar verificar todo el código base en C++ de xrpld. Un oráculo compara entradas equivalentes entre el modelo matemático y la implementación en producción, lo que ayuda a identificar desajustes a medida que evoluciona el software.

Impacto en el mercado

La verificación formal puede reforzar la confianza en la maquinaria de préstamos de XRPL antes de que los validadores activen la enmienda y antes de que se inmovilice más capital de los depositantes. El diseño también está despertando interés comercial de Evernorth y VS1.Finance, lo que aumenta la importancia de una contabilidad de bóvedas predecible.

La prueba tiene límites claros. El reembolso del prestatario, la suscripción y la evaluación crediticia siguen produciéndose fuera de la cadena, mientras que el capital de primera pérdida del intermediario no elimina el riesgo de impago. La verificación puede poner a prueba propiedades y supuestos definidos, pero no puede demostrar que cada prestatario, integración externa o proceso operativo se vaya a comportar de forma segura.