What is formal verification and why it grants absolute correctness end security

Formal verification (FV) is a series of methods and technologies allowing to get much more reliable guarantees of software (or hardware) correctness than traditional approaches based on testing.

The correctness in this case is a correspondence of the behavior to the specification which should be given in a strict and formal way. Traditionally the outcome (main artifact) of the FV process is called the proof and in the deductive branch of the technology it is actually the strict mathematical proof of the software properties which is in turn to be verified by the special software named proof assistants.

Industrial approach suggests the full FV stack consists of

- informal audit

- informal business level specification

- formal engineer level specification

- verification (proof) of the given code against the formal specification

There are a lot of possible ways to perform software verification, all they differ in feasible strictness, potential completeness and deal both with production code or simplified models (used for protocols verification for example). The most methods used in FV are based on contemporary scientific research in mathematics and computer science. The underlying theory is still at the scientific edge under permanent development and have deep influence both on computer science and mathematics itself.

There exists well popular common sense that FV can guarantee absolute correctness if successfully completed. That is only partially true.

The more strict proposition is that deductive FV methods guarantee absolute correctness with respect to the given specification. The quality of the specification itself and it’s completeness and consistency are independent problems, and often the specification good or not-so-good is suggested to be given out of the box, however the FV methods can be applied to assess the specification properties as well. In comparison with testing where only finite subset of cases can be considered, FV deals also with infinite number of cases literally proving the properties for all allowed values of variable parameters of the system. Another important feature of the deductive FV is that it is inheritable: the properties have not to be reverified when embedding the proven subsystem into a bigger one, all statements hold until one changes the code or specification.

The proof itself has not to be analyzed or manually read — the task to verify the proofs is on duty of special very sophisticated software. The consumers of FV results might assess only the specification: if it is good enough and proofs are verified by external proof assistants, the job is well done, and the verified software is assumed to be correct.

P.S. The picture of how neural network imagines formal verification.