Recently, Proof-of-Stake (PoS) consensus mechanisms have been widely adopted by various blockchain platforms due to their superior performance and lower environmental impact. As a relatively new and somewhat unfamiliar consensus mechanism, PoS presents potential security risks. Staking is an extremely important concept in PoS, serving as the entry point to the PoS mechanism. It allows users to lock in their assets to obtain the right to participate in network consensus. As of today, research on it remains limited. Therefore, this paper aims to ensure the security of users’ staked assets and the stability of the consensus network by analyzing the staking mechanism in PoS and modeling a general staking model. We enhance the security attributes of the model by adding a set of high-level properties. Finally, we verify its rationality and effectiveness in the Move language environment.