Efeu: generating efficient, verified, hybrid hardware/software drivers for I2C devices

Writing device drivers is notoriously hard, and driver bugs are a major cause of system failures and vulnerabilities. The problem is particularly acute in bus-based protocols like I2C, where driver correctness is only half the story: correct functioning of the complete subsystem depends on all components on the bus interoperating correctly. Unfortunately, developers cannot control all aspects of a platform, and must interact with existing devices (peripherals and/or hardware bus controllers) which may misbehave. Failures in a protocol like I2C, often used in critical low-level system management, can result in permanent damage to the hardware, whether a server or a satellite.