Alloy Analyzer - if you want to see how far automatic proofs and automatic reasoning on software models have come today, check out this project. Written in Java, installers available for major systems. Comes with a declarative language for model specification and automatic conflict finders - so a faulty model throws out counterexamples that violate at least one of the boundary conditions. And the tutorial doesn't deliver any abstract, practice-remote examples, but for example a model of a date system with various operations on it.