Le préfixe commun vérifie formellement le protocole de prêt adossé au #XRP pour prouver mathématiquement qu’il ne peut pas être vidé, devenir insolvable ou enfreindre ses règles.
Le travail porte sur le protocole de prêt introduit via XLS-66. Le préfixe commun a expliqué son approche dans une série en six volets, notamment pourquoi il a choisi Lean 4 pour le processus de vérification.
Le préfixe commun a déclaré 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.
Le validateur du XRP Ledger, Vet, également connu sous le nom de Hussein Zangana, a indiqué que la vérification formelle est déjà utilisée dans des systèmes à haut risque tels que la technologie militaire, les logiciels de contrôle du trafic aérien, les commandes de vol et les centrales nucléaires.
Il a expliqué que l’approche consiste à utiliser les mathématiques pour démontrer qu’un système reste valide pour toutes les entrées possibles, et pas seulement pour les situations que les développeurs ont testées.
Le préfixe commun a examiné plusieurs outils, dont Dafny, Lean 4, TLA+ et P. L’équipe a décidé que TLA+ et P ne convenaient pas bien aux questions spécifiques auxquelles elle devait répondre au sujet du 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. Le préfixe commun a constaté que le solveur de Dafny pouvait parfois expirer lors du traitement des calculs arithmétiques complexes nécessaires à la vérification. Lean exige davantage de travail manuel, mais cela permet aussi de rendre les erreurs plus faciles à repérer et à corriger pour les développeurs.
#CryptoNewsCommunity
Le travail porte sur le protocole de prêt introduit via XLS-66. Le préfixe commun a expliqué son approche dans une série en six volets, notamment pourquoi il a choisi Lean 4 pour le processus de vérification.
Le préfixe commun a déclaré 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.
Le validateur du XRP Ledger, Vet, également connu sous le nom de Hussein Zangana, a indiqué que la vérification formelle est déjà utilisée dans des systèmes à haut risque tels que la technologie militaire, les logiciels de contrôle du trafic aérien, les commandes de vol et les centrales nucléaires.
Il a expliqué que l’approche consiste à utiliser les mathématiques pour démontrer qu’un système reste valide pour toutes les entrées possibles, et pas seulement pour les situations que les développeurs ont testées.
Le préfixe commun a examiné plusieurs outils, dont Dafny, Lean 4, TLA+ et P. L’équipe a décidé que TLA+ et P ne convenaient pas bien aux questions spécifiques auxquelles elle devait répondre au sujet du 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. Le préfixe commun a constaté que le solveur de Dafny pouvait parfois expirer lors du traitement des calculs arithmétiques complexes nécessaires à la vérification. Lean exige davantage de travail manuel, mais cela permet aussi de rendre les erreurs plus faciles à repérer et à corriger pour les développeurs.
#CryptoNewsCommunity