Dear all, I'm very pleased to announce that scher, the framework I've been working on, has already reached the point where I feel I can present it to the public and ask for feedback. scher is a property-based testing framework for Haskell programs with a similar API as QuickCheck or SmallCheck - the main difference is, instead of random testing, it uses the Klee http://klee.github.io/ engine to perform concolic testing https://en.wikipedia.org/wiki/Concolic_testing, a kind of SMT-enhanced testing which provides greater guarantees than random testing. If you want to get started with it, you will need: * LLVM (I use version 2.9, but you should be able to get 3.4 working with some effort) * Klee * The klee-uclibc https://github.com/klee/klee-uclibc library * my fork of the jhc compiler http://github.com/m-alvarez/jhc, which adds support for running code without a GC * The scher http://github.com/m-alvarez/scher library * The scher-run http://github.com/m-alvarez/scher-run program, which will take care of feeding Klee the right input and formatting the output in a human-readable format. If anyone shows interest, I can write a quick-and-dirty tutorial of the exact list of the incantations you need to get started. As it is right now, everything is experimental and may be subject to change. Furthermore, everything and anything may be broken. Feel free to report any issues, bugs or simply feature requests on GitHub. Any feedback is enormously helpful to me. Happy verifying! -- Now I do not know whether I was then a lambda expression emulating a Turing machine, or whether I am a Turing machine emulating a lambda expression.