github.com/certichain/ceramist ↗

About certichain/ceramist

Ceramist is a Coq library providing formally verified implementations and proofs of hash-based approximate membership query (AMQ) structures. The project formalizes the mathematical properties and correctness guarantees of probabilistic data structures commonly used in computer science, including bloom filters, counting bloom filters, and quotient filters. Each structure is proven to satisfy an abstract AMQ interface with formally verified probabilistic guarantees about false positive rates and other probabilistic behaviors.

The library is built on top of the Coq proof assistant and the coq-infotheo probability library, providing a probability monad and custom tactics to simplify reasoning about probabilistic computations. Key utilities include the comp_normalize tactic for standardizing probabilistic expressions, comp_possible_exists for converting possibility statements into existence proofs, and exchange_big tactics for manipulating nested summations that arise in probabilistic analyses. The development is organized into modular components covering core primitives, utility lemmas, and several instantiated data structures with example applications like BlockedAMQ constructions.

The project is distributed under GPLv3 due to its dependency on the Infotheo library and represents a substantial formal verification effort, with build times around one hour. It serves researchers and practitioners interested in formally verified guarantees for probabilistic data structures, providing both the implementations and machine-checked proofs of their correctness properties.