There's work to address that. Look into proof-carrying code and "fully-abstract compilation." There's also been proofs done for hardware and assembly against sp

There's work to address that. Look into proof-carrying code and "fully-abstract compilation." There's also been proofs done for hardware and assembly against specs in ACL2 and Abstract, State Machines.