I do QA work and for quite some time I have been intrigued by property based testing. But we are usually testing lot of interconnected micro-services and when I tried to define test-scenario in i.e. quick-check, the end-result was always too complicated to maintain.
I basically tried to do a similar thing to John Hughes "Mysteries of Dropbox" paper.
It seems that with temporal logic it would have been much easier to specify the expected behavior of the program and then use the generated trace to instrument the live service and check that all of the properties still hold.
I'd love to see you implement this and write about your experiences.