There are several types of formal methods used to verify a design.
The first is equivalence checking. This takes two designs, that may be at the same or different levels of abstraction and finds functional differences between them. Equivalence checking can be further broken down into two principle domains - combinatorial equivalence checking, often just called equivalence checking, and sequential equivalence checking.
Combinatorial equivalence checking is used to show that a design after logic synthesis is the same as the input RTL description. It is also used to show that no functionality has been affected when test logic or other gate-level transformations are made. It compares the combinatorial logic between corresponding registers in the original description.
Sequential equivalence checking is an emerging technology that can take two designs that have fundamentally different timing, enabling an un-timed or partially timed model to be compared against an RTL model, or between RTL models that have undergone retiming or other transformation to improve power or other design qualities. This is a necessary technology for mass adoption of high-level synthesis.
The other main branch of formal verification is property checking. A property defines a behavior that must be present in a design, or a behavior that must not be possible. A third option is called a fairness condition that would ensure that each of several options is not treated unfairly, in arbitration for example.
In some cases it may be difficult to prove a property and instead of providing a full proof, a bounded proof is all that is possible. A bounded proof may say that the behavior is, or isn't, possible within a defined number of clocks, or from a specific starting state, or when certain constraints are applied to the system.