XRP Ledger testa protocolo de crédito contra risco de insolvência

A Common Prefix está a verificar formalmente o próximo Lending Protocol do XRP Ledger com Lean 4, testando se as suas regras de contabilidade e segurança se mantêm em todos os estados possíveis do sistema. O trabalho surge após o lançamento do xrpld 3.4.0, que inclui LendingProtocolV1_1, uma alteração que ainda precisa da aprovação dos validadores antes de ser ativada.

O protocolo foi concebido em torno de cofres de crédito fechados. Os depositantes podem adicionar ou levantar ativos durante a subscrição, mas o capital fica bloqueado durante o período de investimento e passa a estar disponível para empréstimos sem garantia e com prazo fixo. Os levantamentos são retomados durante o resgate. A contabilidade de caixa regista os juros apenas quando os pagamentos dos mutuários chegam, e não quando os empréstimos são concedidos.

Porque é importante

Falhas contabilísticas nos saldos dos cofres, nos pagamentos dos empréstimos ou nos cálculos das participações poderiam afetar os fundos agrupados dos depositantes. A modelação anterior da Common Prefix revelou violações de invariantes dos cofres, falhas nas asserções relativas a pagamentos de empréstimos, erros de arredondamento aritmético e diferenças entre as especificações escritas e a implementação. A RippleX afirmou que esses problemas foram corrigidos nas versões 3.1.3 e 3.2.0 do xrpld.

O esforço atual recria a lógica relevante do protocolo em Lean 4, em vez de tentar verificar toda a base de código C++ do xrpld. Um oráculo compara entradas equivalentes entre o modelo matemático e a implementação de produção, ajudando a identificar divergências à medida que o software evolui.

Impacto no mercado

A verificação formal pode reforçar a confiança na infraestrutura de crédito do XRPL antes de os validadores ativarem a alteração e de ser comprometido mais capital dos depositantes. O desenho também está a atrair interesse comercial da Evernorth e da VS1.Finance, aumentando a importância de uma contabilidade previsível dos cofres.

A prova tem limites claros. O reembolso pelos mutuários, a avaliação de risco e a análise de crédito permanecem fora da cadeia, enquanto o capital de primeira perda dos intermediários não elimina o risco de incumprimento. A verificação pode testar propriedades e pressupostos definidos, mas não pode provar que todos os mutuários, integrações externas ou processos operacionais funcionarão em segurança.