"Let's call this formula the great implication. If we fail to prove the great implication, it is because the system does not verify the specifications. But if we prove it, we are sure that the system satisfies the specification. Moreover, this proof can be seen as a certificate, which can be communicated and even executed. This technique is also more informative than others; the proof tells us why the system verifies the property, which provides explanatory elements and therefore additional confidence."