<p>Solidity smart contracts are recognized for their susceptibility to vulnerabilities, necessitating thorough verification to mitigate potential security risks. Beyond basic functionality, smart contracts must also adhere to established standards and reflect expected behaviors to ensure proper operation. To address these challenges, adopting a model checking method has proven to be an effective approach. However, the modeling and specification phases demand expertise to achieve rigor. Critical aspects such as inheritance and behavioral factors are often overlooked during the modeling phase, while manual specification can be error-prone and time-consuming. To address these limitations, we introduce <i>SmartGuard</i>, a model checking-based tool for Ethereum smart contracts. Our framework not only examines the functional aspects of Solidity smart contracts but also checks their behavior. Additionally, SmartGuard ensures the correctness of standard-based contracts, providing support for compliance with established standards. To reduce the need for human intervention, we abstract contract models into Behavioral Interaction Priority (BIP) and utilize Large Language Models (LLMs) for formalizing properties into Computation Tree Logic (CTL) formulas. We conducted several experiments that demonstrate the efficiency of the Mistral model to generate CTL properties. Moreover, we evaluate our verification process on several smart contracts showing the effectiveness of our approach. Finally, we conclude with a discussion on future work.</p>