This article talks about design specification and its model-checking; seL4 used a completely different formal method. Formal Methods (for software assurance) i

This article talks about design specification and its model-checking; seL4 used a completely different formal method. Formal Methods (for software assurance) is the name of a research discipline studying the following methods, as well as programming language semantics: * Formal specification of either code or design * Model checking * Sound static analysis * Machine-checked/assisted deductive proof systems and dependent type systems * Concolic testing and automatic test generation * Program synthesis Some of the verification methods above (like some model checkers and sound static analysis) can be used without any explicit specification whatsoever (e.g. they're used to verify lack of undefined behavior in C programs). So the name "Formal Methods" covers a wide range of tools and techniques, with widely varying goals, costs and appropriate domains, that it doesn't really mean much to talk of "formal methods" as if it were a specific thing. Rather, it is a general approach used in constructing widely differing tools and techniques. That's why it's called formal methods, not a formal method.