Most importantly, take a look at High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS) - it specifically discusses a number of formal methods tools.
You may also want to take a look at my essay How to prove stuff.
There are lots of different languages for formally expressing things, just like there are lots of programming languages. You should try to choose the language that most easily represents your needs, but there's a twist: Some of the more expressive languages are harder to automate, so there's a real reason to chose the "least expressive" language so that you can maximally automate.
Many provers are based on "first-order logic" (FOL). If you can express your requirements using some version of FOL, then you can probably use lots of highly-automated tools that actually create the proof (instead of just checking it). Wikipedia's "First-order logic" entry has some useful information.
Here are some external pages on how to convert specs into FOL:
Unfortunately, FOL has some real weaknesses that are easily extended, but many mathematicians don't seem to realize that they are weaknesses. For example, you can't define "if-then-else" easily in FOL. FOL has two "types": formula (essentially booleans) and terms (everything else). You can define a multi-parameter object that returns a boolean (Predicate) or a term (function), but all parameters have to be terms (non-booleans) - and if-then-else inherently takes a boolean! This email notes why it's important to add if-then-else for practical languages. SMT-LIB version 2.0 does add support for an "ite" function of form (ite Bool U U) that returns a U (if Bool is true, it returns the first U, else it returns the second).
Prover9's documentation is a bunch of HTML files; if you want a nice PDF (e.g., to print) with page numbers, table-of-contents, etc., download my scripts make_book and setup_book.pl (make sure you name the file setup_book.pl), install them in the HTML directory files, and run make_book (it presumes Unix-like system; must have htmldoc and perl installed). It will produce a file named "finalbook.pdf".
The prover9 documentation doesn't describe its input format very clearly; here's my attempt at documenting the prover9 formula syntax (in BNF). In the long term, I might switch to TPTP syntax (as Stanford's Computational Metaphysics project has done), since this is a standard format accepted by many tools... but prover9/mace4 include tools to translate to/from TPTP, so I can delay doing that (knowing that I can escape from the unique format of the tool).
There's a paucity of small, simple examples of prover9 in use. Here's the proof that the square root of 2 is irrational, as prover9 input that sqrt(2) is irrational, and here's prover9 output that sqrt(2) is irrational. I created this file, but it's merely a translation of the Otter proof from Larry Wos, by Michael Beeson and William McCune, as published in "The Seventeen Provers of the World" compiled by Freek Wiedijk. I think my translation is much easier to read than the original, because I used traditional first-order operators instead of the lower-level clausal form. Here's the square root of 2 proof, as a graphic.
You can use graphviz to make pretty displays of proofs (see above). My script gvizify takes the XML format that prover9 can create, and generates a graphfiz ".dot" file. You can then run this through "dot" to generate Postscript, PDF, etc. Unfortunately, there seems to be some sort of problem generating PDF files; on my system they often get cropped badly (I'm guessing it's bug 1192, though I don't know if the fault is graphviz, ps2pdf, or somewhere else). For now, to create PDF files I generate Postscript, use "eps2eps" to fix up the Postscript, and then use ps2pdf to create cleaned-up Postscript. That works! You'll need to have graphviz and ghostscript installed. You can use other tools, like Tulip, on the results of graphviz (note: Tulip depends on glew).
My MiniSAT user guide is short, but it's much more than the MiniSAT deveopers provide.
For larger software projects, I like the tools PVS (based on higher-order logic, with types) and ACL2 (based on lambda/LISP) (both GPL licenses). Their languages are more capable than prover9, but in contrast, it can be more work to prove things using them.
ACL2 is intended to be highly automated, and has lots of clever heuristics to handle recursion. ACL2 really shines in dealing with programs that can be easily expressed as pure LISP programs; it's beguiling, really! ACL2 can handle quantifiers ("there exists..." and "for all..."), but quantifiers are at the edge of ACL2's capabilities and are not well-supported by ACL2's automatic proving mechanisms. It's quite a contrast; ACL2 handles recursion well and in many cases automatically (many other systems don't do as well), programming constructs like if-then-else are built-in, and so on... but quantifiers (the basis of most notations) are not ACL2's strength. Also, ACL2 uses LISP notation; a few people like this notation, but the vast majority of people hate this notation as being absurdly hard to read. The LISP notation issue is very solveable; see my readable s-expressions stuff for more about how to solve this.
PVS has a delightfully easy-to-read notation. It supports types and subtypes, and its types are extraordinarily flexible (it's not just "1..10"; you can define "prime numbers" as a type). While PVS wasn't originally intended for directly generating programs, it's been extended so that in certain cases you can generate programs from the specs! It's based on higher-order logic (HOL), which has its plusses and minuses. Its notation is very powerful for expressing things, and that's a plus. But it's not good at automatically proving most things; instead, you have to do much of it "by hand" and it will check/record your work.
See automated theorem proving for general information on that topic.
There are lots of mathematical notations/languages; if you're interested you might look up Second-order logic, Higher-order logic, type theory, Lambda calculus and its variant Typed lambda calculus.
I really want to see powerful notations that can easily describe problems, yet are supported by highly automated tools (so that most of the time, you can quickly determine that a claim is true or find a refutation). I think many of the FOL tools should add capabilities (like if/then/else) that don't make the provers any slower (they often make them faster), but make it much easier to use the tools - that's one immediate way to help. Longer-term, I have high hopes for the various efforts to connect systems with more powerful notations (e.g., higher-order logics like PVS) with first-order logic (FOL) systems. There are lots of papers on such efforts (it's an active area of research). Hurd points to some such work), as does "Combining Proofs of Higher-Order and First-Order Automated Theorem Provers" by Christoph Benzuller1, Volker Sorge2, Mateja Jamnik3, and Manfred Kerber. Hurd separately mentions an interest in translating PVS to an FOL. Meng and Paulson discuss 3 translations. The Proceedings on the 6th International Workshop on the Implementation of Logics is interesting and discusses many efforts to combine approaches (among other things). FOL is more limited, but easier to automate; other notations are easier to use for many problems, but harder to automate in general. In cases where you can convert to FOL, you'll probably be able to do much more automatically, so this appears to me to be a worthy direction.
I hope to get a chance to learn more about SMT-LIB.
You might want to look at my Secure Programming HOWTO web page, Open Source Software and Software Assurance (Security), and High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS).
You can also view my home page.