Reply to Message

http://en.wikipedia.org/wiki/Evaluation_Assurance_Level
Of course the OS he mentions in the article is now the only one in the wiki...
Used to be that a few of the military aircraft operating software appeared in the wiki also.

I think modularity is a better base principle than formal verification.
Cost is less and if you want to achieve formal verification it is simpler to test individual modules. Mathematical simplification can make higher level proofs doable where a less careful module structure could become impossible to proof.