> So the output binary is basically a black box at this point?

To the extent that a formal proof is a black box ... ?

Which leads to an intriguing thought. If our languages and other infrastructure supported formal proofs that compiler output matched input it would obviate the motivation for reproducible builds.