XRPL ищет математическое доказательство того, что его новый рынок кредитования невозможно опустошить

Разработчики XRPL используют математические доказательства, чтобы проверить, можно ли опустошить будущий рынок кредитования или привести его к неплатежеспособности. 17 сентября Common Prefix сообщила, что формально верифицирует протокол кредитования XRPL с помощью Lean 4. Эта работа призвана показать, что протокол не может перейти в состояния, нарушающие его правила учета и безопасности. Версия 3.4.0 включает LendingProtocolV1_1. Поправка добавляет закрытые кредитные хранилища и учет по кассовому методу. Для вступления поправки в силу по-прежнему требуется ее одобрение в рамках процедуры внесения поправок в XRP Ledger. Конструкция кредитования позволяет вкладчикам объединять активы, чтобы кредитные брокеры направляли их на необеспеченные кредиты с фиксированным сроком. Проверка заемщиков и оценка кредитоспособности проводятся вне блокчейна. В реестре фиксируются выдача кредитов, погашения и бухгалтерский учет. В закрытых хранилищах предусмотрены этапы подписки, инвестирования и погашения. Вкладчики могут добавлять активы или выводить их на этапе подписки. Во время инвестирования обе операции заблокированы. На этапе погашения вывод средств возобновляется. График работы хранилища устанавливается при создании и впоследствии не может быть изменен. При учете по кассовому методу проценты признаются только после поступления платежей. В ходе более ранней исследовательской верификации были выявлены нарушения инвариантов хранилищ, сбои утверждений при выплатах по кредитам, ошибки округления в арифметике и расхождения между написанными спецификациями XLS и их реализацией. Common Prefix сообщила, что эти проблемы были устранены в версиях 3.1.3 и 3.2.0. Верификация воссоздает релевантную логику протокола в Lean 4, а не проверяет всю кодовую базу на C++. Оракул сравнивает эквивалентные входные данные математической модели и рабочей реализации. Гарантии распространяются только на определенные свойства и смоделированные допущения. Протокол опирается на внесеточную проверку заемщиков и в настоящее время не использует автоматизированные механизмы обеспечения и ликвидации позиций в блокчейне. Кредитные брокеры могут предоставлять капитал первой потери, однако в документации XRPL говорится, что это не устраняет кредитный риск. Evernorth и VS1.Finance готовятся использовать или создавать решения на базе Single Asset Vaults и протокола кредитования. В конечном счете валидаторы определят, станет ли LendingProtocolV1_1 активным.