We apply infinite-state model checking to formally verify Internet of Things protocols such as the Pub/Sub consistency protocol adopted by the REDIS distributed file system. The verification method is based on a combination of SMT-solvers and overapproximations as those implemented in the Cubicle verification tool.