As KirinDave said, we can apply our tech to as many stages as we like. If applied redundantly, has the extra benefit of verification at one stage catching problems in an earlier one. Far as propagating verification conditions or checking in middle, you might find these concerns addressed by proof-carrying code plus equivalence checks on untrusted optimizations as in VeLLVM. There's also work that equivalence checks transformations in assembly code.

https://news.ycombinator.com/item?id=16041110