These tools and metrics are designed to help AI actors develop and use trustworthy AI systems and applications that respect human rights and are fair, transparent, explainable, robust, secure and safe.
SampCert
SampCert is an open-source, formally verified implementation of algorithms for differential privacy. Differential privacy is a mathematical standard for protecting individuals in data analysis. It works by adding carefully calibrated random noise to query results, so that no single person's data can be identified. The privacy guarantee depends on the noise being generated exactly as the mathematics requires. However, errors in how random sampling is implemented in software can silently weaken this protection. SampCert addresses this risk by providing algorithms whose correctness is mathematically proven. It is used in production in the AWS Clean Rooms Differential Privacy service, which lets organisations analyse shared data without exposing individual records.
SampCert is written in Lean, a programming language and proof assistant, which checks mathematical proofs by computer. The developers use Lean and its mathematical library, Mathlib, to prove that each algorithm behaves exactly as specified. These proofs draw on advanced results, such as the Poisson summation formula.
The verified algorithms include a discrete Gaussian sampler, which generates the random noise used to protect privacy. SampCert also proves key results in zero-concentrated differential privacy, a framework for tracking how much privacy is used up as multiple queries are run on the same data. It also includes a set of verified private queries. The proven code is then compiled into an efficient implementation that can be deployed in real systems. SampCert is released under the Apache 2.0 licence.
Auto-discovered on 2026-08-05 by OECD Catalogue Automation
About the tool
You can click on the links to see the associated tools
Tool type(s):
Objective(s):
Purpose(s):
Country/Territory of origin:
Lifecycle stage(s):
Type of approach:
Maturity:
Usage rights:
License:
Target users:
Risk management stage(s):
Technology platforms:
Github stars:
- 105
Github forks:
- 23
Use Cases
Would you like to submit a use case for this tool?
If you have used this tool, we would love to know more about your experience.
Add use case
Partnership on AI
