Differential privacy is the gold standard for privacy-preserving analysis and also a popular target for the formal verification because of its composition properties. Many tools have been developed that can automatically verify approximate differentially private algorithms, but none of the current state-of-the-art tools give a tight bound on privacy costs for approximate differentially private algorithms. Through this work, we present the theoretical background for a tool that can verify algorithms that use Gaussian noise to be approximate differentially private and provide tight bound on privacy costs. Our approach is to transform a differentially private algorithm into a verifiable version of the algorithm that can be verified using top-of-the-shelf verifiers. Verifiable versions have privacy cost explicit, which can be converted to a curve of possible values of parameters of privacy cost- epsilon, delta. Using the user’s provided budget of values of epsilon, delta we can verify the algorithm to be approximate differentially private. We applied the technique from “optimal accounting of differential privacy via the characteristic function”. We used the characteristic function to characterize privacy loss, which is a lossless representation, which means that, unlike moment-generating functions, characteristic functions always exist. Logarithms of these characteristic functions also compose linearly, which makes privacy tracking easier. The characteristic function is based on dominating pairs - a generalization of worst-case pairs of distributions bounding privacy loss for neighboring datasets. Just like characteristic functions, dominating pairs always exist and compose easily over adaptive mechanisms. In the transformed program, We make privacy cost explicitly by tracking the logarithms of characteristic functions which compose linearly and converting it to epsilon, delta differential privacy. In this work, we extend the simple imperative language introduced in lightDP and shadowDP and also introduce a novel type system. We proved the dominating pair distributions for a simple Gaussian command and the composition of two commands. We used these results to prove the pointwise soundness of the novel type system using proof by structural induction. We also prove the soundness of the type system and explain how our tool can be used to ensure privacy. Our tool is the first one to formally verify approximate differentially private algorithms like the Gaussian mechanism with a tight bound.