> coming up with good properties is not always trivial
This is difficult, but one technique that (might) make it easier for real-world applications beyond simple invariants is to take the approach of building a simple model of the system under test and, in the PBT, checking that your system's behavior matches the model's [1].
Testing behaviour against an 'oracle' is a great class of properties to check.
Especially useful when you want to test an optimized version against a simpler (but slower) baseline version. Or when you have a class of special cases, that you can solve in a simpler way.
Testing the system against itself, but under symmetry, is also useful. But that goes close to general properties. A symmetry could be flipping labels around, or shuffling input order etc; it depends on your system.
This is difficult, but one technique that (might) make it easier for real-world applications beyond simple invariants is to take the approach of building a simple model of the system under test and, in the PBT, checking that your system's behavior matches the model's [1].
[1] https://dl.acm.org/doi/10.1145/3477132.3483540