pith. machine review for the scientific record. sign in

arxiv: 2604.12713 · v1 · submitted 2026-04-14 · 💻 cs.PL · cs.LO

Recognition: unknown

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

Philipp G. Haselwarter , Alejandro Aguirre , Simon Oddershede Gregersen , Kwing Hei Li , Joseph Tassarotti , Lars Birkedal
Authors on Pith no claims yet

Pith reviewed 2026-05-10 13:47 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords differential privacyseparation logicprogram verificationhigher-order functionsprobabilistic programsprivacy filtersSparse Vector TechniqueCoq
0
0 comments X

The pith

A separation logic treats privacy budgets as first-class resources to enable modular verification of complex differentially private programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a program logic for verifying differentially private implementations in general-purpose languages that include higher-order functions and state. It equips the logic with first-class support for privacy budgets as separation logic resources, allowing modular reasoning about individual primitives, higher-order combinators, and interactive algorithms. This expressiveness covers common library patterns such as privacy filters and caching that fall outside prior verification methods. The approach is shown by constructing and verifying a reusable library of mechanisms, including an online Sparse Vector Technique and an OpenDP-inspired privacy filter, with all results foundationally checked in the Rocq Prover.

Core claim

The central claim is that a probabilistic higher-order separation logic with privacy budgets as resources can verify differentially private programs modularly, including those using randomization, local state, and higher-order functions, and that this logic is sound with respect to the standard definition of differential privacy.

What carries the argument

Probabilistic higher-order separation logic in which privacy budgets are modeled as separation logic resources that compose via the separating conjunction, supporting modular specifications for primitives and combinators.

If this is right

  • Specifications for library primitives and combinators can be instantiated to verify clients that use them.
  • Privacy filters that track and enforce budgets across multiple queries can be verified while handling randomization and local state.
  • An online version of the Sparse Vector Technique can be given a modular, reusable specification.
  • Higher-order functions that implement interactive differentially private algorithms become amenable to compositional verification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same resource-based treatment of budgets could be adapted to verify other quantitative properties such as expected error bounds in addition to privacy.
  • The logic's support for local state and higher-order code suggests it could be used to verify differentially private implementations inside existing general-purpose libraries rather than only standalone mechanisms.
  • Because the logic is foundationally verified, its rules could serve as a basis for automated or semi-automated checkers for new differentially private algorithms.

Load-bearing premise

The new separation logic rules are sound with respect to the standard definition of differential privacy and correctly model the semantics of the higher-order probabilistic language with state.

What would settle it

A concrete program that the logic certifies as satisfying a differential privacy specification but that can be shown to violate the standard epsilon-delta guarantee on some input distribution.

Figures

Figures reproduced from arXiv: 2604.12713 by Alejandro Aguirre, Joseph Tassarotti, Kwing Hei Li, Lars Birkedal, Philipp G. Haselwarter, Simon Oddershede Gregersen.

Figure 1
Figure 1. Figure 1: PrivacyFilter ensures that no client can exceed the privacy budget. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The classic Above Threshold interactive mechanism. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: A generic caching mechanism. 1.2 Formal Guarantees for Differential Privacy DP lends itself well to the analysis via standard PL methods due to its compositional nature. We distinguish two main classes of approaches. Type-based approaches [Abuah et al. 2022; Barthe et al. 2015b; de Amorim et al. 2021; Gaboardi et al. 2013; Lobo-Vesga et al. 2020, 2024; Near et al. 2019; Reed and Pierce 2010; Toro et al. 20… view at source ↗
Figure 4
Figure 4. Figure 4: Continuous and discrete Laplacian, with L 𝑚 0.7 (𝑣) for 𝑣=2 and 𝑚 ∈ {0, 1}, demon￾strating 0.7-DP: L 1 0.7 (2) ≤ 𝑒 0.7 · L0 0.7 (2) . We therefore work with the discrete Laplacian ( [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Excerpt of the non-probabilistic rules of Clutch-DP. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Privacy credit laws [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The Above Threshold mechanism. Example 4.1. Suppose we want to privately compute the number of even numbers in a list and check whether it exceeds a threshold of 3. If we run AT with a high privacy budget (e.g., 𝜀 = 10) there is very little noise added and we are very likely to disclose the true result and disclose private information. Concretely, with probability about 92%, above_threshold 10 3 (List.coun… view at source ↗
Figure 8
Figure 8. Figure 8: The Sparse Vector Technique and a streaming client. [PITH_FULL_IMAGE:figures/full_fig_p014_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Privately computing the average of a list of data. [PITH_FULL_IMAGE:figures/full_fig_p015_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Implementations of a Privacy Filter and Adaptive Count. [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Implementations of a cache and a client. [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Comparison of DP systems. “Beyond comp.” = support for mechanisms whose DP goes beyond [PITH_FULL_IMAGE:figures/full_fig_p020_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: The Report Noisy Max mechanism The implementation of RNM takes three arguments: the query function q, the number of queries N, and the database db. The first line of RNM computes the (exact) results of running the query function for all indices 0 ≤ i < N on the database and stores the result in the list xs. The second line pairs each result x with a freshly allocated presampling tape label for a Laplacian… view at source ↗
read the original abstract

Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. However, the design patterns and language features used in modern DP libraries as well as the classes of guarantees that the library designers wish to establish often fall outside of the scope of previous verification approaches. We introduce a program logic suitable for verifying differentially private implementations written in complex, general-purpose programming languages. Our logic has first-class support for reasoning about privacy budgets as a separation logic resource. The expressiveness of the logic and the target language allow our approach to handle common programming patterns used in the implementation of libraries for differential privacy, such as privacy filters and caching. While previous work has focused on developing guarantees for programs written in domain-specific languages or for privacy mechanisms in isolation, our logic can reason modularly about primitives, higher-order combinators, and interactive algorithms. We demonstrate the applicability of our approach by implementing a verified library of differential privacy mechanisms, including an online version of the Sparse Vector Technique, as well as a privacy filter inspired by the popular Python library OpenDP, which crucially relies on our ability to handle the combination of randomization, local state, and higher-order functions. We demonstrate that our specifications are general and reusable by instantiating them to verify clients of our library. All of our results have been foundationally verified in the Rocq Prover.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces a probabilistic higher-order separation logic for modular verification of differential privacy in general-purpose languages with state and higher-order functions. Privacy budgets are treated as first-class separation logic resources, enabling reasoning about DP primitives, higher-order combinators, interactive algorithms, privacy filters, and caching. The approach is demonstrated via a verified library including an online Sparse Vector Technique and an OpenDP-inspired privacy filter; all results, including library and client verifications, are machine-checked in the Rocq Prover.

Significance. If the soundness result holds, the work substantially advances DP verification by supporting complex library patterns and language features outside the scope of prior domain-specific or mechanism-isolated approaches. The foundational Rocq formalization against external semantic models supplies machine-checked evidence for the logic rules, reusable specifications, and modeling of randomization plus local state, which strengthens the central claims.

minor comments (2)
  1. [Introduction] The abstract states that the logic handles 'privacy filters and caching' but the introduction of the privacy filter example could more explicitly note which separation-logic rule (e.g., the resource-splitting rule for budgets) is used to discharge the filter's state update.
  2. [Logic Definition] Notation for the privacy-budget resource (denoted with a separating conjunction) is introduced without a small example derivation in the main text; a one-line derivation showing budget consumption for a single Laplace mechanism would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work and their recommendation to accept the paper. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines a new separation logic for modular verification of differential privacy properties in a higher-order probabilistic language with state. Its central claims rest on the soundness of the logic rules with respect to the standard definition of differential privacy and the language semantics. These properties are established via an independent, machine-checked formalization in the Rocq Prover against external semantic models, rather than by construction, fitted parameters, or self-referential definitions. No load-bearing steps reduce to self-citations, ansatzes smuggled via prior work, or renaming of known results; the derivation chain is self-contained with external verification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central contribution is the definition of a new program logic; it rests on standard background theories of separation logic and probability rather than ad-hoc fitted constants or new physical entities.

axioms (1)
  • standard math Standard axioms and rules of higher-order separation logic and probabilistic semantics
    Invoked as the foundation upon which the new privacy-resource rules are added.
invented entities (1)
  • Privacy budget as a first-class separation logic resource no independent evidence
    purpose: To enable modular splitting, passing, and composition of privacy budgets in higher-order code
    Core new concept introduced by the logic; no independent empirical evidence is provided beyond the formalization itself.

pith-pipeline@v0.9.0 · 5586 in / 1305 out tokens · 49153 ms · 2026-05-10T13:47:35.294946+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages

  1. [1]

    Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal

    Approximate Relational Reasoning for Higher-Order Probabilistic Programs.Proc. ACM Program. Lang.9, POPL, Article 41 (Jan. 2025), 31 pages. https://doi.org/10.1145/3704877 Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal. 2024. Tachis: Higher-Order Separation Logi...

    work page doi:10.1145/3704877 2025

  2. [2]

    VLDB Endow.12, 11 (July 2019), 1371–1384

    PrivateSQL: A Differentially Private SQL Query Engine.Proc. VLDB Endow.12, 11 (July 2019), 1371–1384. https://doi.org/10.14778/3342263.3342274 Elisabet Lobo-Vesga, Alejandro Russo, and Marco Gaboardi. 2020. A Programming Framework for Differential Privacy with Accuracy Concentration Bounds. In2020 IEEE Symposium on Security and Privacy (SP). 411–428. http...

    work page doi:10.14778/3342263.3342274 2019