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