There are no such provably safe programs. I assume that you are thinking about programs that have been verified by formal proof systems. They are not proven to

There are no such provably safe programs. I assume that you are thinking about programs that have been verified by formal proof systems. They are not proven to be safe, they are proven to adhere to whatever the proof system managed to prove. This shifts the possible vulnerabilities away from the actual code and onto the proof system and the assumptions that the proof system makes. For example, take a C program that was proven to be absolutely free of buffer overflows. And therefore labelled by the proof system as 'secure'. But, unbeknownst to the proof system, the C program also interprets user-supplied input as a format string! So it's still vulnerable to format string exploits. Correct proof systems probably add a huge margin of security compared with the current security standards, but it's not absolute.