The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.
[5][6] It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical proof obligations, the truth of which imply conformance of the system to its specification, and discharging these obligations using either proof assistants (interactive theorem provers) (such as HOL, ACL2, Isabelle, Coq or PVS), or automatic theorem provers, including in particular satisfiability modulo theories (SMT) solvers.
Another complementary approach is program derivation, in which efficient code is produced from functional specifications by a series of correctness-preserving steps.
An example of an unsound technique is one that covers only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result.
A variety of techniques are employed, most notably using satisfiability modulo theories (SMT) solvers, and genetic programming,[7] using evolutionary computing to generate and evaluate possible candidates for fixes.
Fault-localization techniques in formal verification are used to compute program points which might be possible bug-locations, which can be targeted by the synthesis modules.
[citation needed] Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation.
Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.
[13][14] In 2016, a team led by Zhong Shao at Yale developed a formally verified operating system kernel called CertiKOS.
[22] The SPARK programming language provides a toolset which enables software development with formal verification and is used in several high-integrity systems.