Formale Verifikation des inkrementellen Merkle-Baum-Algorithmus in Dafny (Eth 2 Einzahlungsvertrag) | Knoovi