The biggest win of predicate-based formal verification (or really any formal verification at all) is forcing you to carefully think about invariants and properties of your code (independently of whether you can prove them). Even if you can't prove them, these serve as useful formal documentation for maintenance purposes and help guide and maximize the efficiency of other techniques such as traditional testing. If you can characterize your code with useful invariants and properties, then you can write useful unit tests and property tests, rather than writing happy path tests that fail to actually catch many bugs.

Assertions are one piece of the puzzle, but often times you want to reason about how something fits in a larger context (the canonical example of this is something like the associativity of an operator, which isn't something you can check for with an assert statement within the operator), which is where independent predicates come in handy.

In general, I think of fuzzing and property-based testing as a lightweight and practical stand-in for the verification part of formal verification. If your formal properties can be proved quickly (e.g. by a short manual proof or some sort of automated engine) then great! If they can't, you can still often times convert it into a fuzzing-friendly format or a property test and get a fairly high degree of confidence of correctness that way.