I2C is a pervasive bus protocol used for querying sensors and actu- ators, but it is plagued with incompatible devices, violating the specification at various levels. Interacting with partially compliant devices poses several challenges. Compati- bility of the master interface, as well as the driver code, must be checked manu- ally and potentially changed. This is a difficult process, as also interactions with other bus devices have to be considered. We propose a model checking approach to quickly write high assurance drivers and layers of the I2C stack. We do not propose single, true formalization of I2C , but a framework that allows to rapidly model non-compliant devices and verify the correct interaction with a host driver process. Our contribution to this is twofold: First, a framework that allows to specify de- vice and driver behavior together, and verify their correct interaction. Second, fine grained building blocks, representing layers of the I2C stack, that are already verified and can be reused to interact with partially compliant devices, as well as reducing model checking complexity. Our specifications are stated in a machine readable, executable and layered DSL. From the DSL, we generate both Promela and C code. The first is used to apply model checking to ensure the layers implementations follow the abstract speci- fications. The second is used to build and verify a EEPROM model and driver running on a Raspberry Pi.