[hnipps]

> The counterexample generator is very powerful because it leverages the knowledge base of the theorem prover (all the accumulated lemmas, etc.) among other things.

That's a really interesting application. Could be very powerful for what I'm doing. Thank you!

[derrak]

Happy to help. In general, I think counterexample generation is more important than proofs when it comes to software (most of our software is “trivially” wrong). The world might not be ready for full-blown formal verification, but I think it is ready for formal specification and counterexample generation.