Very proud of my PhD student Kiran Gopinathan, whose work on verified probabilistic specifications of Bloom filters in Coq just got accepted to CAV'20.

Besides being an impressive piece of proof engineering, this is a remarkable result for the following reasons. 1/6

Bloom filters are one of the most popular probabilistic data structures with False Positive results. Nowadays, they are used everywhere: in networking and consensus protocols, in browsers, in static analysis and even in your favourite blogging platform. 2/6

The main formula that is used by everyone to estimate their False Positive ratio, proved by Bloom himself, is (you guessed it) wrong. This has been known for some time, but the work that claims to have fixed that bound... is also wrong! 3/6

Trying to verify the property as stated in textbooks, we have first independently discovered Bloom's mistake and then, in a hard way, also learned that the follow-up correction also had a bug. Having a fully axiom-free proof in Coq we finally know we got it right. 4/6

But there is more! Most of Bloom filter-ish structures share a common "probabilistic core" wrapped into some non-probabilistic code. This idea allowed us to reuse the proofs between such structures and even engineer completely novel ones, so they are correct by construction. 5/6

The design of our framework, called Ceramist, the decomposition idea, and the case studies, are all described in the paper.
https://ilyasergey.net/papers/ceramist-draft.pdf

The code is publicly available on GitHub and is coming to opam soon.
https://github.com/certichain/ceramist/
6/6