The integration of large language models (LLMs) in smart home systems holds significant promise for automating the generation of Trigger-Action Programming (TAP) rules, potentially streamlining smart home user experiences and enhancing convenience. However, LLMs lack of holistic view of smart home IoT deployments and may introduce TAP rules that result in hazards. This paper explores the application of LLM for generating TAP rules and applying formal verification to validate and ensure the safety of TAP rules generated by LLMs. By systematically analyzing and verifying these rules, we aim to identify and mitigate potential security vulnerabilities. Furthermore, we propose a feedback mechanism to refine the LLM's output, enhancing its reliability and safety in generating automation rules. Through this approach, we seek to bridge the gap between the efficiency of LLMs and the stringent security requirements of smart IoT systems, fostering a safer automation environment.