The ubiquity of the Internet of Things (IoT) and our growing reliance on IoT apps make their dependability more critical than ever. Known for providing the highest degree of software assurance, software verification uses mathematical concepts to prove the correctness of specific properties. Among the notable developments is the emergence of lightweight formal methods, which enable automated, yet formally-precise analysis in an effort to reduce the burden on traditional formal verification techniques. In this talk, I will present the ongoing research in my research group, exploring the possibility of leveraging lightweight formal methods backed by automated program analysis for pragmatic dependability analysis of IoT systems in a compositional and scalable fashion. I will illustrate the ideas in the context of practical applications, discuss their potential for moving the field forward, and pose essential areas of research in the coming era.