After the Intel FDIV bug [1] they started using formal verification to make sure the cpu's did what they said they would. I don't understand why they don't do the same for these avionic systems. Maybe it's just not worth it to the company.
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.
You would be no worse off in this situation. Writing a formal spec. arguably makes it harder to overlook such issues. Formal verification is good at catching things like off-by-one errors, where the problem is not in the spec.
[1] https://en.wikipedia.org/wiki/Pentium_FDIV_bug