I have used it in multiple production systems, even fairly complicated ML-based ones. But also to verify integrity of low-level components that have complex performance optimisations. It has only been met with positive feedback, of the "what a clever way to generate test cases" kind.

The difficult bit is finding invariants or approximations, but doing so is half of what makes the code more robust anyway!

The operational problem is that the tests sometimes take a little longer to run, so sometimes they have to be in a low-prio suite.