The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can.
This is why I like end to end tests, UA testing, fuzzing, and property-based tests.
This is why I like end to end tests, UA testing, fuzzing, and property-based tests.
That is actually the easy part.
From my limited knowledge of formal verification (a university module decades ago and reading the occasional article since) it works very well for individual algorithms or small libraries, where the input ranges and desired outputs can be relatively easy to pin down with some accuracy and precision.
As soon as you are working on something bigger and hairier, even under ideal circumstances the effort to produce the spec becomes exorbitant. And those ideal circumstances include end users (or other stake-holders) who know exactly what they want from the start or at least can be convinced to workshop it (at their cost) until they have bottomed out exactly what they want. More often than not, what happens instead is a PoC is produced, either as wireframes or a fuller prototype, and essentially that PoC and the issues raised against it becomes a partial spec, inconsistencies & holes included. Once you start down that track, getting back towards something formally verifiable is likely harder than starting towards that point in the first place.
IMO formal verification, in an ideal world where you have effectively infinite time for doing things properly properly, or for smaller projects a large but not as infinite time, is the ideal. Unfortunately we don't usually work in an environment like that, so we have to compromise.
The high-water-mark, which is stuff like formal proof of correctness or proof of worst-case runtime, gets a lot of attention; but there are plenty of valuable approaches that are less expensive.
You can do, for example, formal proof of the absence of runtime exceptions (e.g. no bounds check violations), which doesn't require a formal specification and tends to result in a lot of theorems that are easy to prove automatically.
Or you can do data and information flow analysis, which will let you verify that you don't depend on uninitialized values of variables or make sure that your expectations about how different inputs to a program should affect outputs ("hey, why doesn't the weapon release discrete depend on the weight-on-wheels sensor?")
Having done it, I'm pretty sure you can. Why don't you think it can be done?
It requires a programming language (or language subset) with very well-defined semantics, and the use of theorem-proving tools but it's certainly possible.
And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer overruns and use-after-free. Can you determine the absence of race conditions? Can you determine that it meets timing constraints with 100% certainty?
There are a huge number of different kinds of things that a specification could specify. I'm pretty sure that we can't formally verify all of them.
The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.