I am self learning formal methods. I heard that formal methods is used (and usually only used) to create mission critical software (such as nuclear reactor controller, aircraft flight controller, space probe controller). That's why I am interested to learn it :p

However, after learning formal methods (especially LTL, CTL and their siblings), I feel that they can only be used to verify the correctness of the specification (safety, liveness, fairness, etc).

But then how to verify that the software (not only the specification) is indeed correct?

Disclaimer: I am a 90% idiot when it comes to theoretical computer science. So please be merciful while answering.