The characteristic formula of a piece of code is a logical formula that describes the semantics of this code (it is a form of strongest post-condition). This characteristic formula satisfies the following property:

• it is built compositionally and automatically from the source code alone,
• it has a size linear in that of the source code,
• it can be displayed in the logic in a way that closely resembles source code (using Coq notation system),
• it can be manipulated through a small set of specialized tactics that make it unnecessary to know how the formula is constructed
• it is not just a sound, but also a complete description of the code semantics, meaning that characteristic formulae do not restrict in any way the ability to reason about the code;
• it supports modular verification, and it integrates the frame rule, which enables local reasoning.

It is useful to understand what the characteristic formula approach is not:

• it is not a verification condition generator (VCG): the source code needs not be annotated with invariants; instead, invariants are provided in interactive proofs;
• it is not a deep embedding: there is no inductive data type used to represent code syntax, so we avoid all technical issues related to the representation and manipulation of program syntax;
• it is not a shallow embedding: Caml functions are not represented as Coq functions, so there is no need to resort to monadic programming for avoiding the mismatch between program functions, which can be partial, and logical functions, which must be total;
• it is not a dynamic logic: characteristic formulae are not expressed in ad-hoc logic but instead in a standard higher-order logic, making it possible to leverage on existing theorem provers.