The convergence of Internet of Things (IoT) and Home Automation (HA) has revolutionized human-device interaction, typically through Trigger-Action Programming paradigms such as If This Then That (IFTTT). While empowering user-customized automation, this integration introduces critical challenges: unexpected behaviors from improper rule configurations, and cybersecurity threats propagated through interconnected rule chains. Although existing research demonstrates that linear temporal logic (LTL) specifications can formally characterize these risks for model checking verification, conventional methodologies suffer from two fundamental limitations: the inherent state space explosion problem constraining efficiency, and restricted expressiveness of model patterns hindering scalability. Furthermore, the HA-IoT domain notably lacks standardized benchmark datasets for validating LTL-related methods. To address these critical gaps, we propose HAFuzz - an innovative framework that synergizes formal modeling with adaptive fuzzing techniques for efficient temporal specification violation detection. We further incorporate manually curated specifications with large language model (LLM)-driven mutation generation, enabling systematic test case augmentation. Experimental evaluations demonstrate HAFuzz achieves violation detection within 50ms per integration under typical scenarios, showing superior efficiency improvement compared with conventional model checking approaches. Comprehensive validation involving 3,343 LTL specifications confirms HAFuzz’s accuracy and effectiveness in identifying critical violations, particularly in large-scale deployments characterized by intricate rule interdependencies and specifications that feature complex temporal logic patterns.