Common Prefix está verificando formalmente el Protocolo de Préstamos del $XRP Ledger para demostrar matemáticamente que no puede ser agotado, volverse insolvente ni violar sus reglas. El trabajo se centra en el Protocolo de Préstamos introducido mediante XLS-66. Common Prefix explicó su enfoque en una serie de seis partes, incluyendo por qué eligió Lean 4 para el proceso de verificación. Common Prefix señaló que la verificación formal va más allá de las pruebas de software normales al utilizar matemáticas para demostrar que un sistema funciona correctamente en todas las situaciones posibles. El validador del XRP Ledger Vet, también conocido como Hussein Zangana, dijo que la verificación formal ya se utiliza en sistemas de alto riesgo como tecnología militar, software de tráfico aéreo, controles de vuelo y plantas nucleares. Explicó que este enfoque utiliza matemáticas para demostrar que un sistema permanece válido ante todos los posibles inputs, no solo en las situaciones que los desarrolladores han probado. Common Prefix consideró varias herramientas, incluyendo Dafny, Lean 4, TLA+ y P. El equipo decidió que TLA+ y P no eran adecuadas para las preguntas específicas que necesitaba responder sobre el protocolo de préstamos. Una razón por la que eligieron Lean 4 es que no depende de un solucionador SMT. Common Prefix descubrió que el solucionador de Dafny a veces se agotaba al manejar la aritmética compleja necesaria para la verificación. Lean requiere más trabajo manual, pero esto también facilita que los desarrolladores encuentren y corrijan errores. #Ripple https://t.co/s0YcQ4KAWX