Smart contracts, fundamental to blockchain-based decentralized applications, require rigorous correctness and security assurance due to their immutable and self-executing nature. This review paper presents a comprehensive analysis of formal verification techniques for smart contracts, including static analysis, model checking, theorem proving, and symbolic execution. We analyze state-of-the-art tools such as Coq, Mythril, KEVM, and others, comparing their capabilities and limitations. Key challenges in formal verification are identified, including scalability, vulnerability coverage, and tool integration. We also detail real-world incidents such as the DAO Hack and Parity Wallet bug to demonstrate the necessity of these techniques. The paper concludes by highlighting current research gaps and emphasizing the critical need for standardized, scalable, and automated verification frameworks for smart contracts.