Common Prefix формально проверяет протокол кредитования $XRP Ledger, чтобы математически доказать, что он не может быть опустошен, стать неплатежеспособным или нарушить свои правила. Работа сосредоточена на протоколе кредитования, представленном через XLS-66. Common Prefix подробно объяснил свой подход в шестичастной серии, включая причины выбора Lean 4 для процесса верификации. Common Prefix отметил, что формальная верификация выходит за рамки обычного тестирования программного обеспечения, используя математику для доказательства корректной работы системы во всех возможных ситуациях. Валидатор XRP Ledger Vet, также известный как Хусейн Зангана, заявил, что формальная верификация уже применяется в высокорисковых системах, таких как военные технологии, программное обеспечение для управления воздушным движением, системы управления полетом и атомные электростанции. Он пояснил, что этот подход использует математику для демонстрации того, что система остается корректной при всех возможных входных данных, а не только в тех сценариях, которые были протестированы разработчиками. Common Prefix рассмотрел несколько инструментов, включая Dafny, Lean 4, TLA+ и P. Команда пришла к выводу, что TLA+ и P не подходят для решения конкретных вопросов, связанных с протоколом кредитования. Одной из причин выбора Lean 4 стало отсутствие зависимости от SMT-решателя. Common Prefix обнаружил, что решатель Dafny иногда превышал лимит времени при обработке сложной арифметики, необходимой для верификации. Lean требует больше ручной работы, но это также облегчает разработчикам обнаружение и исправление ошибок. #Ripple https://t.co/s0YcQ4KAWX