I just played with this just a few days ago to solve some crackme challenges. It is pretty cool: decompile the binary, use KLEE to symbolize inputs, ..., profit.

There is also DeepState[0], which is quite similar (provides a higher abstraction) for test harnesses

[0]: https://github.com/trailofbits/deepstate/