A verified implementation using Lean and Mathlib of the discrete Gaussian sampler for differential privacy, the composition and postprocessing of zero concentrated differential privacy, and some simple queries.
The Lean implementation is not computable because algorithms that terminate with probability 1 are defined using a combinator. However, the code can be extracted to Dafny and used as part of the VMC library.
Contributors: Jean-Baptiste Tristan, Leo de Moura, Anjali Joshi, Joseph Tassarotti.