There are formally compilers (e.g. CompCert https://en.wikipedia.org/wiki/CompCert ) which are formally proven correct. I think eventually all production compilers will be formally verified.