Over the years I've read that it is possible to proof code similar to the way you can prove a math theorem. I suspect that it can't be done easily for other than the simplest program but at some point in the future automation will be able to do it for a large codebase.
It is a bit scary we are heading into a future where software will dominate most of our life yet software is very easy to break and breach.