Biggest difficulty for me was that some combinations of operations were illegal and I had to think about all the edge cases and filter them out, and this took a long time.
My SO works in hardware, and she says they always use a constraint solver to generate test cases / test vectors, and she never understood why this wasn't popular in software. I googled it a bit and found lots of academic papers but no concrete implementation.
I've also thought about generating test vectors using a generator based on Markov chains, I wrote about that here [0], based on this [1] submission.
I'm not familiar enough with either using constraint solvers to generate test cases, or Markov chains, to know if I'm talking nonsense here or is it just something that nobody thought to develop properly.
Our biggest use case has been testing our database materialization. We have a somewhat complicated hierarchical organization tree/forest within our database. In order to efficiently query those structures, we materialize the transitive closure of these relationships. TL;DR; we populate a row for each (org, ancestor) and maintain that via postgres triggers that fire whenever we mutate things.
The prop test that powers it all does three things. First, it establishes an arbitrary that captures all the possible shapes of organization trees. Second, we define the set of mutations (add a child, switch parents, delete a grandparent, etc.) that may occur. Third, we define code for reading/writing org trees to and from the DB.
The test then generates an org tree, syncs it to the db, performs 1 or more mutations on the tree and then compares what's in the database with the resulting tree.
Overall it's been pretty great. I highly recommend property tests, especially when modeling complex data in an external system.