A verified implementation using Lean and Mathlib of randomized algorithms including the discrete Gaussian sampler for differential privacy, key results in zero concentrated differential privacy, and some verified (unbounded) private queries.
SampCert is deployed and used in the AWS Clean Rooms Differential Privacy service. SampCert proves deep properties about some of its randomized algorithm and makes heavy use of Mathlib. For example, we use theorems such as the Poisson summation formula.
The principal developer of SampCert is Jean-Baptiste Tristan. It is also developed by Markus de Medeiros.
Other people have contributed important ideas or tools for deployment including (in no particular order): Leo de Moura, Anjali Joshi, Joseph Tassarotti, Stefan Zetzsche, Aws Albharghouti, Muhammad Naveed, Tristan Ravitch, Fabian Zaiser, Tomas Skrivan.
To cite SampCert you can currently use the following reference:
@software{Tristan_SampCert_Verified_2024,
author = {Tristan, Jean-Baptiste},
doi = {10.5281/zenodo.11204806},
month = may,
title = {{SampCert : Verified Differential Privacy}},
url = {https://github.com/leanprover/SampCert},
version = {1.0.0},
year = {2024}
}