Der „Common Prefix“ verifiziert den Ledger Lending Protocols (#XRP ) formell, um mathematisch zu beweisen, dass es nicht ausgeraubt werden kann, nicht zahlungsunfähig wird und seine Regeln nicht brechen kann.
Die Arbeit konzentriert sich auf das Lending Protocol, das über XLS-66 eingeführt wurde. Der „Common Prefix“ erläuterte seinen Ansatz in einer sechsteiligen Serie, darunter auch, warum er Lean 4 für den Verifizierungsprozess gewählt hat.
Der „Common Prefix“ sagte, formale Verifikation gehe über normales Software-Testing hinaus, indem sie mit Hilfe von Mathematik beweist, dass ein System in allen möglichen Situationen korrekt funktioniert.
Der XRP-Ledger-Validator Vet, auch bekannt als Hussein Zangana, sagte, dass formale Verifikation bereits in sicherheitskritischen Systemen wie Militärtechnik, Software für den Luftverkehr, Flugsteuerungen und Kernkraftwerken eingesetzt werde.
Er erklärte, dass der Ansatz Mathematik nutzt, um zu zeigen, dass ein System über alle möglichen Eingaben hinweg gültig bleibt – nicht nur über die Situationen, die Entwickler getestet haben.
Der „Common Prefix“ prüfte mehrere Tools, darunter Dafny, Lean 4, TLA+ und P. Das Team entschied jedoch, dass TLA+ und P für die spezifischen Fragen, die es zum Lending-Protocol beantworten musste, nicht gut geeignet waren.
Ein Grund für die Wahl von Lean 4 war, dass es sich nicht auf einen SMT-Solver stützt. Der „Common Prefix“ stellte fest, dass Dafny’s Solver manchmal ein Time-out verursacht, wenn es die komplexe Arithmetik bewältigen muss, die für die Verifizierung erforderlich ist. Lean erfordert zwar mehr Handarbeit, macht aber auch Fehler leichter auffindbar und für Entwickler einfacher zu beheben.
#CryptoNewsCommunity
Die Arbeit konzentriert sich auf das Lending Protocol, das über XLS-66 eingeführt wurde. Der „Common Prefix“ erläuterte seinen Ansatz in einer sechsteiligen Serie, darunter auch, warum er Lean 4 für den Verifizierungsprozess gewählt hat.
Der „Common Prefix“ sagte, formale Verifikation gehe über normales Software-Testing hinaus, indem sie mit Hilfe von Mathematik beweist, dass ein System in allen möglichen Situationen korrekt funktioniert.
Der XRP-Ledger-Validator Vet, auch bekannt als Hussein Zangana, sagte, dass formale Verifikation bereits in sicherheitskritischen Systemen wie Militärtechnik, Software für den Luftverkehr, Flugsteuerungen und Kernkraftwerken eingesetzt werde.
Er erklärte, dass der Ansatz Mathematik nutzt, um zu zeigen, dass ein System über alle möglichen Eingaben hinweg gültig bleibt – nicht nur über die Situationen, die Entwickler getestet haben.
Der „Common Prefix“ prüfte mehrere Tools, darunter Dafny, Lean 4, TLA+ und P. Das Team entschied jedoch, dass TLA+ und P für die spezifischen Fragen, die es zum Lending-Protocol beantworten musste, nicht gut geeignet waren.
Ein Grund für die Wahl von Lean 4 war, dass es sich nicht auf einen SMT-Solver stützt. Der „Common Prefix“ stellte fest, dass Dafny’s Solver manchmal ein Time-out verursacht, wenn es die komplexe Arithmetik bewältigen muss, die für die Verifizierung erforderlich ist. Lean erfordert zwar mehr Handarbeit, macht aber auch Fehler leichter auffindbar und für Entwickler einfacher zu beheben.
#CryptoNewsCommunity