一句话：在 Lean 中机械化差分隐私基础，并提供经形式验证的 Laplace 与高斯采样实现。
差分隐私（DP）是隐私保护数据分析的金标准，但正确实现十分困难：已有验证常假设基础理论正确或噪声源完美，而基本机制与随机数生成缺陷会导致真实漏洞。本文提出 SampCert，首个面向可执行 DP 实现的综合性机械化基础。它用 Lean 编写，含超过 12,000 行证明，提供通用可扩展的 DP 定义，可实例化为纯 DP、集中 DP、Rényi DP 等；给出机制构造与组合框架，以及形式验证的离散 Laplace 与高斯采样算法，避免浮点实现陷阱。SampCert 引入概率 monad 与新的证明技术，并复用 Mathlib 的傅里叶分析、测度概率、数论和拓扑定理。其验证算法已用于 AWS 的 DP 服务。
Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifying DP at a high level, assuming either that the foundations are correct or that a perfect source of random noise is available. However, the underlying theory of differential privacy can be very complex and subtle. Flaws in basic mechanisms and random number generation have been a critical source of vulnerabilities in real-world DP systems. In this paper, we present SampCert, the first comprehensive, mechanized foundation for executable implementations of differential privacy. SampCert is written in Lean with over 12,000 lines of proof. It offers a generic and extensible notion of DP, a framework for constructing and composing DP mechanisms, and formally verified implementations of Laplace and Gaussian sampling algorithms. SampCert provides (1) a mechanized foundation for developing the next generation of differentially private algorithms, and (2) mechanically verified primitives that can be deployed in production systems. Indeed, SampCert’s verified algorithms power the DP offerings of Amazon Web Services, demonstrating its real-world impact. SampCert’s key innovations include: (1) A generic DP foundation that can be instantiated for various DP definitions (e.g., pure, concentrated, Rényi DP); (2) formally verified discrete Laplace and Gaussian sampling algorithms that avoid the pitfalls of floating-point implementations; and (3) a simple probability monad and novel proof techniques that streamline the formalization. To enable proving complex correctness properties of DP and random number generation, SampCert makes heavy use of Lean’s extensive Mathlib library, leveraging theorems in Fourier analysis, measure and probability theory, number theory, and topology.
@article{paperbot3087,
title = {Verified Foundations for Differential Privacy},
author = {Markus de Medeiros and Muhammad Naveed and Tancrède Lepoint and Temesghen Kahsai and Tristan Ravitch and Stefan Zetzsche and Anjali Joshi and Joseph Tassarotti and Aws Albarghouthi and Jean-Baptiste Tristan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729294}
}