Smart contracts, a core component of blockchain platforms, enable automated and immutable execution of decentralized applications. However, many vulnerabilities in smart contracts originate from flawed access control mechanisms, such as missing checks, conflicting rules, or privilege misuse. To address this challenge, we propose an Event-B–based framework for formally specifying and verifying smart contract access control policies at the design phase, ensuring their soundness before deployment. Unlike existing analysis approaches that detect vulnerabilities post hoc, our approach provides a mathematically rigorous foundation that guarantees correctness through step-wise refinement, formal proof, and verified Solidity code generation. The framework has been evaluated through a case study, demonstrating its ability to detect design flaws early and establish a verified foundation for implementation. Compared with existing frameworks such as VeriSolid and Zeus, SmartContract2Event-B performs full proof-based consistency verification instead of bounded model checking, offering stronger soundness guarantees and improved pre-deployment reliability.