Formal Modeling of Staking and Validator Creation in PoS System

Abstract

Blockchain Technology has presented a tamperproof and secure structure that supports the modern digital environment. Among the many consensus blockchain systems, the Proof of Stake (PoS) has emerged as an extensively used protocol due to its lower energy consumption and high security. However, the staking mechanism and creation of the validator process are the main parts of the PoS network, and any flaw in these processes can cause financial loss and breach the system's security. Therefore, we use formal verification methods for the verification and validation of the staking mechanism. In this study, we presented a formal model of staking processes in a PoS-based system, emphasizing the verification of accurate signer, stake allocation, creation of a validator with an NFT minted, and update timeline. The CSP\# language is used to specify these processes, and Linear Temporal Logics (LTL) are used to define the properties against these specifications. To verify that the system satisfies the critical properties, like verification of an authentic signer, secure stake registration, and deadlock-free validator creation using the Process Analysis Toolkit (PAT) model checker, and ensure the system's liveness and safety. Our results describe the importance of formal verification in enhancing the Polygon Blockchain's integrity by ensuring the staking mechanism in the stake manager contract is secure and reliable.