[Taikonerd]

The VST Lab at Princeton works on this sort of problem: https://vst.cs.princeton.edu/

"The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context."

Some of the same researchers worked on TAL (typed assembly language), which sounds like it could be one of the "intermediate representations" you mentioned.