With the explosive growth of the second generation blockchain platforms and applications, smart contracts as executable code deployed in the blockchain are facing more and more security problems. At present, most of the researches on the security of smart contracts focus on the mining of security vulnerabilities, while insufficient attention has been paid to the impact of the fairness of smart contracts on security. To address this problem, a fairness verification method based on model checking is proposed, which is used to verify the fairness of Puzzle contract, and a known transaction order dependency vulnerability is found. The results show that the proposed method can provide a new idea for verifying the fairness of smart contracts.