Formally verified code is awesome. It moves the `debugging problem' up one level, "Does our formal spec capture our informal meaning?"

Ideally in practice, that problem is simpler than "Does our code what we want?

In theory in the abstract, of course, the problems are the same.