Compared to software formal methods have greater adoption. But there are a lot of things that fall under the “formal” umbrella.

The most common type that is used would probably be logical equivalence checking. Proving RTL and a netlist are equivalent is useful for catching synthesis bugs.

Or proving two netlists are equivalent after inserting test functions directly into a netlist, or some other netlist edit.

Property checking is what I use the most. You can check these during simulation which I wouldn’t call “formal” but you can also prove them using tools that use SAT solvers and whatnot to prove things mathematically.

As always, the tricky part of verification is writing the correct test or model. With formal we can use SystemVerilog assertions to write properties and sequences, but the difficulty in getting them right goes from trivial -> inscrutable very quickly.

It’s extreme easy to write assertions that pass and never realize your assertion was not doing what you thought and you weren’t proving what you meant to.

I haven’t used some of the more advanced tools so maybe they have ways to make this easier. But because of this I tend to just write assertions that are pretty easy to understand at a glance, and therefore closer to the trivial side of things.

If a peer has to solve a sudoku puzzle in their head to understand your work, then it’s unlikely the peer review will be worth anything. So I do what I can to make my work understandable at a glance (from a competent peer in the industry).

Of course making something simple can be quite challenging and often takes more time than leaving something complex and opaque.

I’ve never been involved in the foundry side of the work, and for ASICs, that is often half of the schedule.