本文针对使用高斯分布的差分隐私算法的验证问题展开研究。现有形式化验证方法在处理连续分布（尤其是高斯分布）时面临精度和可判定性挑战。作者提出了一种新颖的近似方法，用于逼近无循环程序的概率分布，这些程序可从具有可计算概率密度函数的离散和连续分布（包括高斯和拉普拉斯）中进行采样。他们证明了对于这类程序，验证 (ε,δ)-差分隐私是“几乎可判定的”，即除有限个δ值外，所有情况均可判定。验证算法通过结合积分近似和尾部概率界，以任意所需精度计算概率。该方法已在工具 DipApprox 中实现，利用 FLINT 库进行高精度积分计算，并包含提升可扩展性的优化。作者在基础隐私保护算法上验证了工具的有效性，如稀疏向量技术的高斯变体和 Noisy Max，展示了其在确认隐私保证和检测违规方面的能力。该研究为差分隐私机制的自动化验证提供了理论保证和实用工具，适合形式化方法研究者和隐私保护工程师阅读。