There's SPARK (http://spark-2014.org/ http://spark-2014.org/) that's an Ada dialect with verification features, and there's frama-c, doing something similar for

There's SPARK (http://spark-2014.org/ http://spark-2014.org/) that's an Ada dialect with verification features, and there's frama-c, doing something similar for C (http://frama-c.com/ http://frama-c.com/). In both cases the compiler is pretty much part of the trust base (which is a problem because they're annoyingly complex), but the issues discussed here are declared invalid by the subset (ie. you mustn't use statements that may lead to undefined behavior). For seL4, mentioned in another comment, there was proof that interesting properties of the high-level code and the low-level binary were equivalent. That only works with a relatively static compiler version and for some optimization levels (anything that optimizes too globally will seriously mess up such attempts of showing equivalence), but it takes the compiler out of the trust base.