SampCert is a verified implementation of randomized algorithms including the discrete Gaussian sampler for differential privacy, key results in zero concentrated differential privacy, and some verified (unbounded) private queries using Lean and Mathlib. Lean is a modern, functional, dependently-typed programming language that allows both to write efficient code (with a foreign function interface to C), but at the same time can serve as a proof assistant, via the proofs-are-programs principle.

Read the Paper on Verified Foundations, try out SampCert and write some additional examples on top of the existing ones. Two possible ideas are:

  1. Do the Lean Numbers Game to learn basic Lean proofs – then write about how to go from simple, easy Lean theorems to SampCert theorems.
  2. Find an alternative differential privacy tool (maybe an older, simpler / or a newer, better one), write example programs / proofs in both and compare them.