El prefijo común está verificando formalmente el protocolo de préstamos del Ledger #XRP para demostrar matemáticamente que no puede drenarse, volverse insolvente ni romper sus reglas.
El trabajo se centra en el Protocolo de Préstamos introducido a través de 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 dijo que la verificación formal va más allá de las pruebas normales de software al usar matemáticas para probar 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 control de tráfico aéreo, controles de vuelo y plantas de energía nuclear.
Explicó que el enfoque utiliza matemáticas para demostrar que un sistema sigue siendo válido en todas las entradas posibles, 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 una buena opción para las preguntas específicas que necesitaba responder sobre el protocolo de préstamos.
Una razón por la que eligió Lean 4 fue que no depende de un solucionador SMT. Common Prefix descubrió que el solucionador de Dafny a veces podía agotar el tiempo de espera al manejar el complejo cálculo aritmético necesario para la verificación. Lean requiere más trabajo a mano, pero esto también facilita que los desarrolladores encuentren y corrijan errores.
#CryptoNewsCommunity
El trabajo se centra en el Protocolo de Préstamos introducido a través de 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 dijo que la verificación formal va más allá de las pruebas normales de software al usar matemáticas para probar 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 control de tráfico aéreo, controles de vuelo y plantas de energía nuclear.
Explicó que el enfoque utiliza matemáticas para demostrar que un sistema sigue siendo válido en todas las entradas posibles, 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 una buena opción para las preguntas específicas que necesitaba responder sobre el protocolo de préstamos.
Una razón por la que eligió Lean 4 fue que no depende de un solucionador SMT. Common Prefix descubrió que el solucionador de Dafny a veces podía agotar el tiempo de espera al manejar el complejo cálculo aritmético necesario para la verificación. Lean requiere más trabajo a mano, pero esto también facilita que los desarrolladores encuentren y corrijan errores.
#CryptoNewsCommunity