Differential privacy is defined by comparing a mechanism’s output distributions on neighboring datasets, but the mechanism analyzed on paper is not always the one that runs in software. A real implementation samples from finite random primitives, rounds values, executes rejection loops, and returns machine-representable outputs. These choices can change the set of observable outputs and their probabilities, so a proof for an ideal distribution does not automatically certify the implemented mechanism.

The projects that follow address this gap at different levels. Statistical auditing searches for neighboring inputs and output events that contradict a claimed privacy guarantee, while relational verification proves privacy by reasoning about paired executions under explicit program semantics. Other work examines what additional information is already contained in private outputs: analyses of joint distributions and shared randomness enable richer reporting and adaptive reuse without additional privacy loss. Studies of exact sampling and floating-point side channels then bring the analysis to the implementation itself, where sampling procedures, finite arithmetic, and output encoding determine the distribution that the code actually exposes.