Smart contract is a computer protocol running on the blockchain, which is widely used in various fields. However, its security problems continue to emerge. Therefore, it is necessary to audit the security of a smart contract before it is deployed on the blockchain. Traditional testing methods cannot guarantee the high reliability and correctness required by smart contracts. This study shows how to use modeling, simulation, and verification language (MSVL) and propositional projection temporal logic (PPTL) to model and verify smart contracts. First, the theoretical basis of MSVL and PPTL is introduced. Then, by analyzing and comparing the characteristics of solidity and MSVL, an SOL2M converter which can convert a solidity program to an MSVL program is developed and its design idea is introduced in detail. Finally, the execution results of SOL2M converter are given by two examples of a vote smart contract and a bank transfer smart contract. The properties of contracts are described by PPTL on three aspects:function consistency, logic correctness, and contract completeness. And the process of using UMC4M (Unified Model Checker for MSVL) to verify the contract is also given.