Advances and standards in Internet of Things (IoT) have simpliﬁed the realization of building automation. 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 paper presents our experience in running a building automation service based on the Salus framework. Complementing eﬀorts that simply verify the IoT control system correctness, Salus takes novel steps to tackle practical challenges in automated debugging of identiﬁed policy violations, for non-expert IoT users. First, Salus leverages formal methods to localize faulty user-programmable logics. Second, to debug these identiﬁed faults, Salus selectively transforms the control system logics into a set of parameterized equations, which can then be solved by popular model checking tools or SMT (Satisﬁability Modulo Theories) solvers. Through oﬃce deployments, user studies, and public datasets, we demonstrate the usefulness of Salus in systematically debugging the correctness of IoT control systems for building automation.