If you have a model of the programming language, then you can make proofs about the source code itself. At this point, your assumption is that you are accuratly modelling the compiler.

You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.