In particular I liked the idea of negative testing: making sure bad things don't happen, even if you generate data from a wider domain than what a function is meant to support.
The targeted property-based testing example is really impressive. The author tests a version of Quickcheck, and asks the framework to target a high runtime, putting an assertion in the test to make it fail if the runtime is very high. The framework then goes and generates an example of data causing O(n^2) behavior in quickcheck. Just beautiful.
I'm not done with the stateful testing part, but already I applied some of the stuff to a Python project (using Hypothesis) with good results. I hope I get to apply it to Elixir in the future.
Some tools are starting to emerge, like gnatstack for Ada & Spark that gives (or tries to give you) the maximum stack size, statically - a parallel step to compilation, like the Spark examiner and prover). It's very limited in my opinion (some dynamic-sized object returned on the stack are not handled yet, function pointers, I don't have the list handy but it was quite limited). You can get similar stuff (less integrated) with gcc options, IIRC.
There's also all the work on WCET that might get interesting but modern architectures are so complex and changing that I'm not sure we'll get near ubiquitous, user-friendly availability for those tools in the near future (next 10 years). For the time being it's mostly used in 'hard' safety-critical projects (avionics), especially since multicore, deeply pipelined architectures, with shared resources (memory, cache, buses) are getting used more and more and they're harder to predict than the previous architectures.
I've been using property testing to issue random workloads and test some of our work software, already it has found some bugs.
Like with certain kinds of unit testing, I have the sense that the process of using a property testing framework has beneficial effects while a system is under development which aren't exactly clear to see from the artifacts of the final committed code and tests since by then you've dealt with a bunch of edge cases the tests told you about and have refactored / rewrote / removed things. So try it! Even if you don't commit it. And anyway the "trivial" problems are still worthwhile too (like catching errors in a pair of serializer/deserializer classes for some custom data), and like other kinds of tests it's best for your properties to be short and easy to read.
I think the chief difficulty is just adjusting to thinking in terms of "properties" that are worthwhile to check. The examples here (and summarized in the quicktheories readme) are good starting points. Also it's more on the toy example side but I've personally made an analogy to Polya's How to Solve It introductory problem of finding the diagonal length of a box. He lists a bunch of other mathematically interesting things you can do with the solution besides just use it to solve the one problem, and most of those things could be encoded into properties. (Like, is the solution symmetric (shuffling around the box's length/width/height values doesn't change the answer), if you increase the height does the diagonal's length increase, if you scale all three sides does the diagonal scale the same amount, does it solve a related problem of the diagonal of a rectangle (box with height 0), are you using all the given data in the solution...) A point is that the math problem doesn't end with giving the answer, and similarly testing doesn't stop after you've verified the happy case or fulfilled some coverage requirement.