The website [1] is worth reading too.<p>I like the idea of an automated prover and an SMT solver running concurrently, one looking for a proof and the other for a counter example.<p>[1] <a href="http://cosette.cs.washington.edu/" rel="nofollow">http://cosette.cs.washington.edu/</a>