We summarize the first DeepSpec project output that covers the whole scope envisioned for the larger effort, though with significantly simpler pieces, and only involving separate subteams within one of our institutions (though we promise that there was a genuine integration challenge here across artifacts that had been designed and implemented separately!). We introduced the project at last year’s DeepSpec workshop, and now the proofs are all connected and free of axioms beyond standard ones. The system is a controller for a lightbulb, accepting commands over an Ethernet card. We started by building the whole thing with conventional tools, beginning with a commercial RISC-V microcontroller, programmed with GCC-compiled C code. Then we replaced the hardware and software pieces separately with implementations inside Coq, showing that each could be dropped in to work properly with its mainstream counterpart. We designed a modular proof structure to help connect application code, device drivers, compiler, and processor without committing in advance to the profile of attached devices.