I just wish HN were more about this and less about "iOS7". Sometimes the amount of Apple zealots around here frightens me, who would support a company like that, and the NSA stuff sharing space with their stuff is quite a fit.
Apparently the version of CompCert from 2007 (before any optimizations) took 2 person-years to write. But some of those persons were pretty impressive.
This took person-years of time from people who already were Coq experts.
SLAM basically models the NT kernel and the Win32 API and checks for loads of bugs.
 Satisfiability Modulo Theories
The core of the xmonad window manager was verified with Coq (PDF):
There are a bunch of examples in the Archive of Formal Proofs: http://afp.sourceforge.net
And some tutorials:
Generate OCaml code from Coq:
Proof algorithms written in OCaml using Coq:
Write program specification and use multiple provers (including Coq):
Write certified programs, and verify proofs using Coq:
Language semantics / type system proofs of languages:
http://www.cl.cam.ac.uk/~so294/ocaml/ (for a subset of OCaml)
Books on Coq:
Coq and TLA+ obviously solve different problems, so comparing them directly isn't possible. For a first step into formal methods for distributed systems engineers, however, I'd recommend TLA+ based on my experiences.
What on earth were you thinking naming it "Coq"?
"The word coq means "rooster" in French, and stems from a tradition of naming French research development tools with animal names. It is also a reference to Thierry Coquand, who developed the aforementioned calculus of constructions along with Gérard Huet. Also, at first it was simply called Coc, the acronym of calculus of construction."
> At this stage of the chicks' development, the cocks usually has begun to enter the nest to help his hen in caring and feeding the chicks.
"Cock" as a word is no different from "bitch" or "stud:"
We should perhaps invade them and teach a thing or two about American culture.