Our paper on mechanised verification of probabilistic properties of Bloom filters and their generalisations has been accepted to CAV 2020.