Proving the Above Threshold algorithm to be differentially private using the Approximate Relational Hoare Logic (apRHL) in the EasyCrypt repository.

The epsilon parameter will differ depending on the proofing technique.