Obligatory reference to previous HN discussion of Reflections on Trusting Trust by Ken Thompson [1]. I'd be interested in any war stories or links to compilers

Obligatory reference to previous HN discussion of Reflections on Trusting Trust by Ken Thompson [1]. I'd be interested in any war stories or links to compilers verified with things like: Cryptol [2], Coq [3] or Idris [4]. I've seen Cryptol prove equivalence for cryptographic algorithms written in C and Java. Would love to learn more about how this approach can or can't be applied to compilers. 1. https://news.ycombinator.com/item?id=2642486 https://news.ycombinator.com/item?id=2642486 2. http://www.cryptol.net/ http://www.cryptol.net/ 3. https://coq.inria.fr/ https://coq.inria.fr/ 4. http://www.idris-lang.org/ http://www.idris-lang.org/