Vérification formelle de l'algorithme d'arbre de Merkle incrémental dans Dafny (Contrat de dépôt Eth 2) | Knoovi