Property based testing is useful for finding bugs even in these kinds of CRUD heavy apps. There can be a surprising number of bugs and unexpected behaviors in the interaction of multiple sub-systems or APIs, and one way to find those bugs is to come up with properties on traces of calls.

For example, I saw a paper on using metamorphic testing (a particular technique for defining properties to test) to find bugs in the web APIs of Spotify and YouTube[1]. I don't have time to reread the paper just now, but I remember that they found weird behavior in pagination of search results. Not a big deal in that particular case, but I've definitely seen internal APIs with behavior that could be similarly wrong but with a much larger real-world impact.

[1]: https://ieeexplore.ieee.org/document/8074764

Personally, I see property-based testing and formal specification more as tools for design and debugging more than full-on correctness. Even with AI models it's still really hard to fully prove something correct, but having even a partial logical specification can let you trade design time for debugging time and lets you find inconsistencies or potential edge-cases when you're initially figuring out a system, rather than waiting until you have a massive codebase to debug and redesign in production.

It's not a panacea and you still have to be careful at the boundary between your nicely modeled system and the real world, but, once I got the hang of working in that style, having some formal properties or partial logical specifications of the behavior I needed has been really nice to have, as much for saving effort as for ensuring correctness.

I've mostly worked in slightly different domains, but I've found property-based testing useful both as a tool to catch bugs but also as a tool for communication. I spent a couple of years building and supporting a supply chain simulation at Target, where I frequently got requests for new metrics from the supply chain planning team. By teaching them how to specify either the whole metric or, at least, some of the expected behaviors of the metric as mathematical properties, it took far fewer back-and-forth conversations to correctly implement the metric in the simulation. We could then test these things by checking these properties over a bunch of random simulation traces. Day-to-day this saved a bunch of time in debugging small simulation mistakes. In the longer-term, having this test suite also let us rewrite the simulation code in a new style in Rust to drastically increase performance. All of this would have been possible without the set of properties, it would have just involved a whole lot more slow, tedious work.