> This is an easy mistake to make. Note the word distinct: > each message in the set to be stored is hash coded into a number of distinct bit addresses Good p

> This is an easy mistake to make. Note the word distinct: > each message in the set to be stored is hash coded into a number of distinct bit addresses Good point, You are right that our correction does not address errors in Bloom's original definition, but rather in the definition of the Bloom filter that is typically used - I'll add a note to address this. > My broader point though was about your "guarantee that there are no further hidden errors", because a theorem prover is just a tool, tools are used by people, and people make mistakes. Yes, you are right, that's probably too strong a claim, my aim was to emphasize that there is more certainty in the proof, making it unlikely that there are no further hidden errors, but that was not clear.