PAR platform is a software platform developed by our research team to support software formality and automated development. The platform fully embodies the advantages of functional abstraction and data abstraction, thus making software development convenient and reliable. The key to achieving this performance is a batch of reusable software components. In order to ensure the correctness and reliability of the whole software platform, it is very important to ensure the correctness and reliability of the software components. In this paper, we select some typical software components in the PAR platform, formalize the semantics of the components in a formal way, and prove the correctness of the components with the help of the Coq theorem prover, hence improving the efficiency of software compoents’ formal verification.