The VST Lab at Princeton works on this sort of problem: https://vst.cs.princeton.edu/ https://vst.cs.princeton.edu/ "The Verified Software Toolchain project as

The VST Lab at Princeton works on this sort of problem: https://vst.cs.princeton.edu/ 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.