# CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples

arXiv: https://arxiv.org/abs/2008.07485 · HTML: https://mlsanity.com/paper/2008.07485/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Aug 2020.

## Built on by (most cited first, 7 of 7)

- [How reparametrization trick broke differentially-private text representation learning](https://mlsanity.com/paper/2202.12138/) (2022)
- [PPA: Preference Profiling Attack Against Federated Learning](https://mlsanity.com/paper/2202.04856/) (2022)
- [Revisiting Differentially Private Hyper-parameter Tuning](https://mlsanity.com/paper/2402.13087/) (2024)
- [The Hitchhiker's Guide to Efficient, End-to-End, and Tight DP Auditing](https://mlsanity.com/paper/2506.16666/) (2025)
- [QueryCheetah: Fast Automated Discovery of Attribute Inference Attacks Against Query-Based Systems](https://mlsanity.com/paper/2409.01992/) (2024)
- [Learning Differentially Private Mechanisms](https://mlsanity.com/paper/2101.00961/) (2021)
- [Sequential Auditing for f-Differential Privacy](https://mlsanity.com/paper/2602.06518/) (2026)

## Abstract (arXiv)

We propose CheckDP, the first automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to automatically generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and more precise in catching infrequent events than existing counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.