There's just always a "who watches the watcher" recursive paradox with formal specification / verification. Who ensures the specification is a good one? I beli

There's just always a "who watches the watcher" recursive paradox with formal specification / verification. Who ensures the specification is a good one? I believe it is just that - a logical paradox. It cannot be answered. We will always have to be double-checking the specifications, perhaps via model checking. All that's to say, I agree with you, it's not like this is going to solve all problems just by using formal specs.