The neverending stream of exploits based on undefined behavior proves you wrong. There is not a single widely used codebase that is completely free of UB and doesn't come with a formal proof.