Vadhan, SalilWood, PhilipFeng, Amy2026-07-0720262026-06-022026Feng, Amy. 2026. Verification of OpenDP Transformations. Bachelors Thesis, Harvard University Engineering and Applied Sciences.32574352https://dash.harvard.edu/handle/1/42743980Differential privacy (DP) is a method of releasing statistical information about a dataset while concealing the properties of individual data records. OpenDP is an open-source repository that allows an individual or organization to easily apply differential privacy to their statistical releases. OpenDP's transformations are a key part of manipulating datasets while ensuring differential privacy properties. Because OpenDP is used on potentially sensitive datasets, it is important to ensure that the OpenDP code is completely sound. As a first step toward formal verification of the OpenDP code, we translate the pseudocode for OpenDP functions into Lean and prove their correctness.application/pdfenComputer scienceThesis or Dissertation2026-07-07