Nope. CompCert is an example of software that was mostly proven correct (all the important stuff) and zero bugs have ever been found in the proven correct parts. So yes you can indeed write zero bugs software.