How do I know the formal specification is what I actually wanted?
Is the connection between the informal requirements to the formal specification easier to trace/follow than the connection between the informal requirements and the code?
There are two separate problems here - one is that you might not be able to clearly explain what you actually want. The other is that you might simply fuck up when writing the formal spec (code). Formal verification is meant to assist you in the latter - when you know what you want, but can make mistakes writing it down, or not realize your description is self-contradictory in some aspects.
Code is a formal specification. You can have layers of such specifications. The problem with viewing code as the specification is that a lot of languages obscure the intent and only reveal the how.
I'm working on a radio product, it's clear how data is being moved into certain buffers. It's clear when data is moved into certain buffers. It isn't clear why data is moved into certain buffers, or if the code is correct, only that it's being done.
A higher level specification set allows us to have a documented understanding of why the code does what it does, and allows us to reason about it at that level. It also makes it feasible to bring new people into the project, because 150k sloc (not a huge project, but not small) of largely low-level code is not something someone new can jump in on and understand quickly.
We also have something that's much easier to reason about when designing system tests, and to test the code against. We write the tests as though the specification were the reality, and test the code against that model to detect where it diverges. If we only had the code, what would we test it against? If it's its own spec, then it can't be wrong.
Yes, people tend to forget that. Having a second formal specification can be helpful, because writing things down multiple times (differently) often helps understanding.
What I've seen so far is that (non-code) formal specs can be very useful when the domain is highly technical, for example network protocols, because they illuminate aspects that are hidden in "production" code.
Of course the fact that important aspects are hidden is a more general problem.
Where did the formal specification come from?
How do I know the formal specification is what I actually wanted?
Is the connection between the informal requirements to the formal specification easier to trace/follow than the connection between the informal requirements and the code?