Hi there,
1. Learn formal verification say Equivalence Checking starting from small HDL programs. Always prefer to work on one tool at a time. (Quality, not Quantity matters).
Per se, Start over with Cadence Conformal.
2. Equivalence Checking verifies the equivalence between two views say - RTL vs Netlist , RTL1 vs RTL2 , Netlist1 vs Netlist2. It is tool independent until you are using same RTL Code, Technology Library and Any 1 synthesis tool for all Formal Tools.
3. There is nothing like language, the commands will vary between different Vendors/Tools. If you know how to show equivalence, in say Conformal, definitely, same thought process can be used in solving it in other Tool.
Is this info sufficient ?. Let me know if you want to know more.