Assuming you can formally prove the software*, all that does is show that the software matches the specifications. Not that the specifications are right in the first place.
[*] Formally proving software isn't easy. It's not as if, in your IDE, you go Tools -> Prove and get a simple box back saying "Proved Correct"
Biting the hand that feeds IT
