One of two cases: pushing Verilog through yosys-smtbmc to check design assertions/properties, or writing a lil Python model of some optimisation trick and checking it's equivalent to a more direct implementation.

For the former it's useful when there's already a well-defined contract at some interface, like "this bus interface follows these basic AHB5 manager rules" or "if x_valid is asserted, it remains asserted until x_ready is asserted, and the other x_foobar are stable during that time" or "a FIFO is never both empty and full".

Simple properties + exhaustive checking is good bang-for-buck because it often teases out subtle tangential issues without having to write checks for implementation details. This isn't "formal verification" per se but using formal checks in a lightweight way to help find bugs and inconsistencies in your design.