Common Prefix vérifie formellement le protocole de prêt du $XRP Ledger pour prouver mathématiquement qu’il ne peut pas être vidé, devenir insolvable ou enfreindre ses règles. Le travail se concentre sur le protocole de prêt introduit via XLS-66. Common Prefix a expliqué sa méthode dans une série de six articles, y compris les raisons pour lesquelles il a choisi Lean 4 pour le processus de vérification. Common Prefix a indiqué que la vérification formelle va au-delà des tests logiciels classiques en utilisant les mathématiques pour prouver qu’un système fonctionne correctement dans toutes les situations possibles. Vet, validateur du XRP Ledger également connu sous le nom de Hussein Zangana, a déclaré que la vérification formelle est déjà utilisée dans des systèmes à haut risque tels que les technologies militaires, les logiciels de gestion du trafic aérien, les systèmes de contrôle de vol et les centrales nucléaires. Il a expliqué que cette approche utilise les mathématiques pour démontrer qu’un système reste valide pour toutes les entrées possibles, et non seulement pour les scénarios testés par les développeurs. Common Prefix a examiné plusieurs outils, notamment Dafny, Lean 4, TLA+ et P. L’équipe a jugé que TLA+ et P n’étaient pas adaptés aux questions spécifiques qu’elle devait traiter concernant le protocole de prêt. L’une des raisons pour lesquelles elle a choisi Lean 4 est qu’il ne repose pas sur un solveur SMT. Common Prefix a constaté que le solveur de Dafny pouvait parfois dépasser le délai d’attente lorsqu’il traitait l’arithmétique complexe nécessaire à la vérification. Lean exige plus de travail manuel, mais cela permet également aux développeurs de détecter et de corriger plus facilement les erreurs. #Ripple https://t.co/s0YcQ4KAWX