A natural target for formal methods has been correctness proofs of
systems that combine hardware and software components, which
indeed is one of the main goals of the DeepSpec effort.
Well-known examples in this space include the CLInc stack verified
by J Strother Moore and associates in the 1980s, with the
predecessor tools of ACL2.  That development wasn't particularly
modular, in the sense of supporting low-cost reconfiguration of
proofs to fit new stacks with significant component reuse from
past examples.  I will explain progress at MIT on interfacing
hardware and software proofs in more modular styles that are
popular today at conferences like PLDI.  The central interface
point is the formal semantics of the machine language, which can
be used to state proof obligations for both a processor and a
compiler.  We have developed simple prototypes of both, sufficient
to support basic Internet-of-things applications, and we are
working toward finishing the end-to-end correctness result.