Mizar

Magnitude 2 star forming the middle joint of the Big Dipper. Right next to it is a considerably dimmer star named Alcor which was used by ancient optometrists as an eye test - your vision was considered normal if you could distinguish the one from the other. Classically the pair have been called "Horse and Rider."

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?