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.
The assertion is that they're lightweight formal methods. Or is the article (and the proceedings of SOSP '21 it links to) wrong?
EDIT: ah I see where there might be confusion--obviously a library for generating random test data and making assertions about code under test itself doesn't constitute anything like "formal methods" but the idea of using that library in the way described in the paper linked from the article does. But that's kinda always the thing about software libraries..
Not sure what exactly you mean by "necessary", but I feel like the entire field of mathematics would disagree. Proving statements about infinite domains has a very long tradition.
The notion of a proof and verification of a real-life software are almost completely disjoint.
Of course, if you are interesting in proving statement about abstractly defined constructs: infinity is no issue as your domain is uniform. In real-life, this is not the case.
