A very powerful proof checking system (software). It is used at the University of Alberta for CMPUT 270, Formal Systems and Logic, and possibly other courses. It's hosted on the university's Solaris and FreeBSD systems; however, the source is available, and it has been ported to just about everything.
The syntax is fairly simple. A series of semicolon delimited statements makes up a proof. Each makes an assertion and backs it up by referring to other statements by label. There is also slightly more complicated syntax for subderivations and other more powerful tools, allowing fairly sophisticated proofs.
Recently however, rumours have surfaced that it is no longer used at any other universities and that it is no longer accepted as trustworthy by the scientific community. Perhaps someone can comment?