I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash.

Similarly, if I make a change which I don't expect to change the output of the parser, then I can use this test suite to be quite sure that my change hasn't changed behaviour.

One thing I am unclear about is what it means for klee to be "done" on my binary. When it has generated all the test cases, if none of them crash my binary, then does that mean it is impossible to crash my binary in 10 bytes of input?

You can find both interesting uses (esp extensions) and users on the page below:

http://klee.github.io/publications/

There's a large amount of work building on KLEE. Similarly, it builds on LLVM that has its own huge ecosystem. The potential of all that together is what interests me about it.

More people are using cbmc, the non-llvm variant, but otherwise very similar tool. I find cbmc much easier to use.