CompCert is written in Coq, and was developed as a research project at academic institutions [1]. It's a very small program (about 1/5 the size of jQuery) that has taken world-experts years to develop.

[1]: https://en.wikipedia.org/wiki/CompCert