Skip to content

markusdemedeiros/SampCert

 
 

Repository files navigation

SampCert

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}
}

About

SampCert : Verified Differential Privacy

Resources

License

Citation

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 95.6%
  • Python 3.8%
  • Other 0.6%