I also think property based testing is great.

But they are very different IMO at what they focus on and so they occupy different places when talking about does a piece of software does what it should do and withing the state/parameters specified:

- Property based testing focuses on finding counter examples - Formal verification focuses to prove that a property always holds

More than this I think in all these discussions we are missing the most important piece: validation.

While verification means to prove or test or verify that the software does what is should do, validation means to prove or test or verify that the software is solving user needs.