What if you can't take control of the program, like Ironsides? It seems as if your premise is that it's too complex to verify the application layer. However, you don't need to model every behavior in a program and this can be leveraged to reduce proofing overhead. A recent paper [1] produced <100 line security proofs for an SSH server, http server, and the SOP of a web browser.

1: https://pdfs.semanticscholar.org/bc9c/491e215d4abad1be7de944...