Forget hair. Sand works better!

In layman's terms, formally proven software is software written twice, once as a formal specification, and once as code, and then the two are proven to be equivalent. This is a labour-intensive way to write software, and it makes bugs much less likely, but it's not perfect: there can be corresponding errors in both the code and the specification, and there can be errors in the proof too. But nothing is perfect, and this certainly can be a good approach to write code that is as close as possible to bug-free.