The fungible contract tokens encounter numerous security challenges due to the vulnerabilities in contract languages; while Move, a novel and secure contract language, is designed to mitigate these vulnerabilities theoretically. To verify the security of the Move-based contract coin, this paper employs formal methods to model the Aptos coin, a leading Move-based token, and assess its high-level properties. Firstly, we examined Aptos Coin’s contract code and integrated the Move’s characteristics to construct a bottom-up model. Subsequently, we specified the necessary high-level properties that the model should possess. Finally, we utilize the Move Prover, a model-checking tool to verify the essential secure properties of Aptos coin. The results demonstrate that the Aptos coin can satisfy the properties with few prerequisite conditions.