I think formal verification brings a bit more to the table. The logical properties are not just a second implementation. They can be radically simpler. I think quantifiers are doing a lot of work here (forall/exists). They are not usable directly in regular code. For example, you can specify that a shortest path algorithm must satisfy:

    forall paths P from A to B:
        len(shortest(A,B)) <= len(P)

That's much simpler than any actual shortest path algorithm.