SampCert: Verified Foundations for Differential Privacy (PLDI 2025) (dl.acm.org)

SampCert is a PLDI 2025 contribution that builds a mechanized, end-to-end foundation for proving differential privacy (DP) properties of randomized programs. The authors present a formal framework inside a proof assistant that encodes the standard ε/δ DP definitions, the key proof principles (relational reasoning/couplings), and common mechanisms and transformations used in practice — including additive-noise mechanisms, composition rules, and amplification-by-subsampling results. SampCert also provides a certificate format and toolchain that links machine-checked proofs to concrete implementations, so a developer can obtain a verifiable privacy certificate for a randomized algorithm rather than relying on pen-and-paper proofs. This matters because DP proofs are subtle and easy to get wrong; mechanized verification both raises assurance and scales reuse of privacy lemmas across projects. Technical highlights include a formalization of probabilistic couplings and privacy loss analyses within the logic, mechanized proofs of standard theorems (composition, advanced composition, subsampling amplification), and a pathway to automatically check that a program’s implementation matches the proven specification. For the AI/ML community, SampCert lowers the barrier to shipping provably-private training and analytics pipelines by turning informal DP arguments into machine-checked certificates that can be integrated into development and audit workflows.