Formal verification plays a crucial role in cryptography by providing detailed methodologies to guarantee the correctness and security of cryptographic protocols. In an increasingly digital world where sensitive information is constantly transmitted and stored, the significance of formal verification cannot be underestimated. By providing us with an elaborative mathematical proof, formal verification helps in constructing authentic cryptographic protocols, which can be deployed In real world applications. The goal of our research is to use EasyCrypt, the interactive theorem prover, to formally analyse and prove the security of modular succinct proof systems. These proof systems serve as essential components in cryptographic protocols, enabling efficient and verifiable computations while preserving privacy and integrity. Through the formalization of these systems, our ultimate research objective is to establish a solid foundation for proving the security properties of deployed cryptographic systems, thereby reinforcing their trustworthiness in practical applications. Our current research efforts are focused on proving the security properties of two polynomial commitment schemes, namely PolyCommit_DL (Discrete Logarithm) and PolyCommit_Ped (Pedersen Commitment), within the EasyCrypt environment.