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.

Formal verification is important because it can help to detect and prevent software errors that might lead to system failures, security vulnerabilities, or other negative consequences. By proving the correctness of a program, formal verification can provide a high level of assurance that the program will work as intended in all circumstances.
Formal verification is particularly useful in safety-critical applications, such as aircraft control systems, medical devices, and nuclear power plants, where even a small software error could have catastrophic consequences. In such applications, it is essential to ensure that the software is correct and reliable, and formal verification provides a rigorous and systematic method for achieving this.
How is Formal Verification Used in Practice?
Formal verification is typically used in conjunction with other software engineering techniques, such as testing, code reviews, and static analysis.
Formal verification is a powerful technique that can help to ensure the correctness and reliability of computer programs. By providing a rigorous and systematic method for verifying program correctness, formal verification can help to prevent software errors that might lead to system failures, security vulnerabilities, or other negative consequences. While formal verification can be complex and time-consuming, it is an essential tool for developing safe and secure software in a wide range of applications.


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