Property tests are informal tests of formal properties. They don't guarantee the properties hold, or that the formal properties are complete, but they exploit the existence of these formal properties.
Once you have formal properties, you can write property-based tests using them, and I wonder how much of the benefit of formal methods could be obtained just by doing this. It's another example of using increased computing power (testing) to substitute for expensive hand labor (proving theorems).
I'll also observe that even theorem proving systems benefit from a kind of property based testing. If there's a goal to prove the existence of a value satisfying some property, this is essentially a property based testing problem. Similarly, find a counterexample to a universally quantified formula (also an existential problem) can be used to prune off unproductive branches of a search tree.
There's something also in the UX dynamics. As a developer writing property based tests I'm encouraged to think much more carefully about system invariants, otherwise there's not much value added over unit tests. For anything nontrivial this entails building a model of the system and checking it against the system under test, like they did at AWS. So the decision to use this tool shapes how you think about the system--it makes you reason more formally about it rather than just winging it and writing tests to exercise the code.
Once you have formal properties, you can write property-based tests using them, and I wonder how much of the benefit of formal methods could be obtained just by doing this. It's another example of using increased computing power (testing) to substitute for expensive hand labor (proving theorems).
I'll also observe that even theorem proving systems benefit from a kind of property based testing. If there's a goal to prove the existence of a value satisfying some property, this is essentially a property based testing problem. Similarly, find a counterexample to a universally quantified formula (also an existential problem) can be used to prune off unproductive branches of a search tree.