Comment by IshKebab

I don't think they are underrated. They are heavily used where they work really well and bugs have a very high cost (e.g. hardware design).

For the vast majority of software though they don't really make much sense because formally verifying the software is 10-100x more work than writing it and testing it with normal methods. And formal verification of software generally requires faaaaar more expertise than most people have. (The situation is much better for hardware design because it tends to be way simpler.)

It's a very powerful tool but also extremely difficult to use.