Differential Privacy not only ensures the anonymity of data, but provides a way of rigorously quantifying and proving how private released information is. A drawback of Differential Privacy is that most suggested implementations are formalized using real numbers. This makes Differentially Private algorithms unimplementable on finite machines. A common way to get around this issue is to implement these algorithms using floating point numbers. However, as shown by Ilya Morinov, these naive implementations lead to privacy breaches using an attack on the least significant bits of the floating point numbers. Therefore, finding ways to verify implementations of Differential Privacy is of significant interest to many. Using Coq, we have formalized a version of the Geometric Truncated Mechanism (GTM), first suggest by Arpita Ghosh, Tim Roughgarden, and Mukund Sundararajan using fixed precision arithmetic, and verified that the GTM is in fact Differentially Private.