There are verified compilers such as the compcert compiler and also ways to verify that a given binary does in fact correctly implement an specification