Formal Verification of Solidity Smart Contracts via Automata Theory

Smart contracts, as a critical application of blockchain technology, significantly enhance its programmability and scalability, offering broad application prospects. However, frequent security incidents have resulted in substantial economic losses and diminished user trust, making security issues a key challenge for further development. Since smart contracts cannot be modified after deployment, flaws in their design or implementation may lead to severe consequences. Therefore, rigorous pre-deployment verification of their correctness is particularly crucial. This paper explores the symmetry in control flows and state transitions of Solidity smart contracts and leverages this inherent structural symmetry to develop a normalized state transition model based on a finite state machine. The FSM model is subsequently formalized into a Promela model with the Spin model checker. By integrating manually defined Linear Temporal Logic formulas with those generated by Smart Pulse, the Promela model is formally verified in Spin to ensure the correctness and security of smart contracts. This approach establishes a systematic verification framework, providing effective support to enhance the reliability and security of smart contracts.