Would you say that this has limitations and it's not a silver bullet? Eg. What if your software added numbers, formal verification proved that your program was indeed correct because it added the numbers. However, it missed the requirement that you also had to do subtraction, which for some reason was omitted in the specification.