My master's thesis advisor (http://www.cs.ttu.edu/~rushton/) is interested in formal verification. This is the most practical and informative introduction to formal verification that I've seen yet. All the talks about formal verification using Mizar/PVS/ACL2/etc. that I've attended have been over my head and utterly impractical. The Coq documentation, even though at first glance is still over my head, is much more approachable than the Mizar documentation I've seen. Thanks for the link!
