Formal verification techniques come under the Verification stage as per your flow..
The usual standard verification techniques involve providing a test vector ( or a wave form) to the Design and observing the out put for any failures. So one can say the Correctness of the design is proportional to the coverage of your test vector.
In Formal verification techniques, instead of test vectors the tool checks that if certain basic conditions defined by the user are met ( or not voilated ) under all circumstances. Mind you this is not a explorative procedure but a exhuative procedure as thing like binary decision trees , state space explosion etc are used to check the correctness of the circuit mathematically.
There are a couple of techniques such as static assertion based verification, and dynamic assertion based verification in which the user can define assertions such as "A should always be 1", or "A'B = 0" then the engine check that such assertion should never fail...
1. after the buffer insertion, cts... compared the generated netlist is functionally the same as data-in
2. after eco
3. last check before tapeout
of course you can check your rtl code is same with the gate level too... but I don't use it often.
Sometimes, we used it for re-writing codes... but it's not very useful... ;(