cbmc: <a href="http:&#x2F;&#x2F;www.cprover.org&#x2F;cbmc&#x2F;applications.shtml" rel="nofollow">http:&#x2F;&#x2F;www.cprover.org&#x2F;cbmc&#x2F;applications.shtml</a>
cmbc is easiest to install, they even have binaries.
easy samples also in the manual: 
<a href="http:&#x2F;&#x2F;www.cprover.org&#x2F;cprover-manual&#x2F;modeling-assertions.shtml" rel="nofollow">http:&#x2F;&#x2F;www.cprover.org&#x2F;cprover-manual&#x2F;modeling-assertions.sh...</a><p>klee: <a href="https:&#x2F;&#x2F;klee.github.io&#x2F;tutorials&#x2F;" rel="nofollow">https:&#x2F;&#x2F;klee.github.io&#x2F;tutorials&#x2F;</a>
pretty hard to install<p>coq: <a href="https:&#x2F;&#x2F;coq.inria.fr&#x2F;a-short-introduction-to-coq" rel="nofollow">https:&#x2F;&#x2F;coq.inria.fr&#x2F;a-short-introduction-to-coq</a>
the real beast out there. easy to install. but hardly usable for normal hackers, because of their mathematical notation.
but it&#x27;s using plain c, and you can verify c with various solvers.<p>z3: <a href="http:&#x2F;&#x2F;rise4fun.com&#x2F;z3&#x2F;tutorial" rel="nofollow">http:&#x2F;&#x2F;rise4fun.com&#x2F;z3&#x2F;tutorial</a>
the most popular, but only python or SMT-LIB 2.0 (lisp).<p>for crypto <a href="https:&#x2F;&#x2F;srlabs.de&#x2F;minisat-intro&#x2F;" rel="nofollow">https:&#x2F;&#x2F;srlabs.de&#x2F;minisat-intro&#x2F;</a> has some explanation how to break weak ciphers or hashes, knowing the weakness beforehand. but the various hackers posting on their blogs usually have better practical explanations.