Advances and standards in Internet of Things (IoT) have simplified the realization of home automation (HA). However, non-expert IoT users still lack tools that can help them to ensure the underlying control system correctness: user-programmable logics match the user intention. In fact, non-expert IoT users lack the necessary know-how of domain experts. This talk presents our MenShen framework which conducts the verification and debugging of HA-IoT system automatically. First, MenShen builds the formal model of the HA-IoT system automatically. Then, off-the-shelf model checkers can be utilized to check the correctness of the system. Last but not least, to debug the identified faults, MenShen selectively transforms the control system logics into a set of parameterized equations, which can then be solved by popular model checking tools to synthesize fix suggestions for non-expert users.