Synopsys has a production grade C-to-RTL sequential equivalence tool called HECTOR, with a focus on data path verification.

https://blogs.synopsys.com/from-silicon-to-software/2021/02/...

So do Cadence with Jasper C2RTL. (Disclaimer; I work on Cadence Jasper Apps, formerly JasperGold)

https://www.cadence.com/ko_KR/home/tools/system-design-and-v...

Nice, thanks guys!

This is the easiest way to get an idea for what is happening and what experience is needed:

https://jobs.apple.com/en-us/search?search=formal&sort=relev...

There are several different niches, and HW formal is likely using different tools and methods than SW formal, though there is overlap. Anyways there is room for a wide range of experience/skills/background in a variety of different areas.

Chisel usage rounds to zero in my estimation.