if you are asking how Formal verification tools basically work, here is a general idea.
First of all, as dave_59 said, you have to "tell" the Formal tool your design SPEC, such as bus protocol, constraints, what is expected, or what is not expected, etc.
After you specify your design in a format that formal tool understands, the tool would usually take your design, and enumerate ALL possible "legal" inputs per your "SPEC", then check if the result is legal. If it is not, the tools will usually provide you some information to debug.
Formal verification is very useful on clearly-defined interface, like connections, or AXI bus. But it is limited in high demand of CPU/memory resources for a medium-complexity design, as well as proving scenarios involving long-loop feedback logic, let alone system behavior.