I believe (no real proofs as I'm not in EDA maerketing/data collection) Cadence's IFV is quite popular as well. Few companies in Bangalore use it. ALso Jasper's tools are popular in the US (not in India).
The formal verification tool is depends on the which tool u r using for the synthesis.if ur using synopsys tools for synthesis then u have to use "formality" tool.if ur using RTL-compiler u have to use LEC from candence. so if ur using some companie synthesis tool u recomended to use same companie synthesis tool .
If so you should clearly spec out what are the eval criteria and proceed - statistics are great, but not so much useful when it comes to tool purchase - as they say "Your mileage may vary", so I would draft a clean eval criteria and proceed. If I were you I would include:
1. Jasper
2. Cadence IFV
3. 0-In
4. Magellan
as a minimum list to get best for my bucks.
BTW - I've used 4 formal tools - IFV, @HDL @Verifier, Safelogic/Jasper Verifier, Solidify (Averant) and can help you with your eval, if interested let me know!