In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods.

System types that are considered in the literature for formal verification include finite state machines (FSM), labelled transition systems (LTS) and their compositions, Petri nets, timed automata and hybrid automata, cryptographic protocols, combinatorial circuits, digital circuits with internal memory, and abstractions of general software components.

The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL) or computational tree logic (CTL).

Usually formal verification is carried out algorithmically. The main approaches to implementing formal verification include state space enumeration, symbolic state space enumeration, abstract interpretation, abstraction refinement, process-algebraic methods, and reasoning with the aid of automatic theorem provers such as HOL or Isabelle.

Validation and Verification

Verification is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V.

Validation: "Are we building the right product?", i.e., does the product do what the user really requires.

Verification: "Are we building the product right?", i.e., does the product conform to the specifications.

The verification process consists of static and dynamic parts. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic).

Validation usually can only be done dynamically, i.e., the product is tested by putting it through typical usages and atypical usages ("Can we break it?").