Hi @jamey,
You mentioned our Termite work and ask what happened to it.
Termite had three issues:
1. the (initially very fruitful) collaboration with Intel died before we could get our hands on real device implementations to generate correct specs
2. the synthesis wasn't really the way to go to create good drivers (was attempted to mitigate with the developer-guided synthesis, but only to a limit)
3. it never managed to deal with DMA (that one's bbviously the real killer)

We re-started the driver verification work a few years ago, and now have solutions to all this:
1. we've got a process (which is being further automated) for extracting provably-correct specs from the Verilog source, see https://trustworthy.systems/projects/deviceformalisation/. We've successfully applied it to open-source I2C and (almost complete) SPI controllers, and are targeting a commercial Ethernet controller next
2. we've created for seL4 a driver model that makes it far easier to write correct and performant drivers manually (like Termite making use of the learnings from Dingo), see https://trustworthy.systems/projects/drivers
3. we now have a verification approach that can deal with DMA (and are close to completing verification for a high-performance Ethernet driver)