How to Create Mission Critical Software? 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.
The question is rather broad.  To answer it in a reasonable space I will make many oversimplifications.

Let us agree on terminology.  A program is correct when it implies its specification.  This vague statement is made precise in many ways, by pinning down what exactly is a program and what exactly is a specification.  For example, in model checking the program is a Kripke structure and the specification is often an LTL formula.  Or, the program could be a list of PowerPC instructions and the specification could be a set of Hoare-Floyd assertions written in, say, first-order logic.  There are very many possible variations.  It is tempting to conclude that in one case (Kripke structure) we do not verify an actual program, while in the second case (list of PowerPC instructions) we do.  However, it is important to realize we really are looking at mathematical models in both cases, and this is perfectly fine.  (The situation is quite similar to physics where, for example, classical mechanics is a mathematical model of reality.)

Most formalizations distinguish between the syntax and the semantics of a program; that is, how it is represented and what does it mean.  The semantics of a program is what counts from the point of view of program verification.  But, it is of course important to have a clear way of assigning meanings to (syntactical representations of) programs.  Two popular ways are the following:


(small step) operational semantics: This is very much like defining a programming language by writing an interpreter for it. For this you need to say what is the state, and it is affected by each statement in the language.  (You may wonder in which language you write the interpreter, but I'll pretend you aren't.)
axiomatic semantics: Here each statement type comes with an axiom schema. So, roughly, whenever a particular statement of that type is used, it translates in being able to use certain axioms.  For example, the assignment ${\bf x}:={\bf e}$ comes with the schema $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$; the particular assignment $x:=x+1$ comes with the axiom $\{x+1=1\}\,x:=x+1\,\{x=1\}$ if we instantiate the schema with $P=(x=1)$.


(There are others.  I feel particularly bad for omitting denotational semantics, but this answer is already long.)  Machine code plus operational semantics is pretty close to what most people would call a ‘real program’.  Here is a seminal paper, which happens to use operational semantics for a subset of the DEC Alpha machine code:


Necula, Lee, Proof-Carrying Code, 1996


Why would you ever use some higher-level semantics, like the axiomatic ones?  When you do not want your proof of correctness to depend on the hardware on which you run.  The approach then is to prove correctness of an algorithm with respect to some convenient high-level semantics, and then prove that semantics sound with respect to lower-level semantics that are closer to actual machines.

In summary, I could think of three reasons that led to your question:


You saw only high-level semantics that don't look like what you are used to call a program, and you wonder if there are low-level ones.  The answer is yes.
You wonder how you prove that a model corresponds to reality.  Like in physics, you don't.  You simply come up with better models and check them against reality.
You have not seen the distinction between syntax and semantics, and various ways to assign meanings to programs.  Two previous questions list some books.


This answer is merely trying to identify three different ways in which I understood the question.  Going deep in any of these points would require a lot of space.