Coq is is a proof assistant for computer assisted verification of mathematical proofs. The home page is http://coq.inria.fr (where an easy-to-install OSX version can found). Proofs are written in the special-purpose lambda-calculus-like language 'gallina'. coqtop is the top level command interpreter for coq.
A Coq mode for Alpha is in development, featuring a coq console for interaction with coqtop. The most interesting aspect of this mode is perhaps the step-console functionality (described on the page Pipes.StepConsoles). It also illustrates the strictConsole package (included): a mechanism that prevents anything from being typed above the prompt in a shell-like window.
Coq mode, which requires AlphaTcl from CVS HEAD newer than 2005-03-08, can be downloaded from http://mat.uab.es/~kock/alpha-tcl/coq.tar.gz . Included is an example file giving a formal proof of the commutativity of 2-monoids (the Eckmann-Hilton argument). You can play with the step functionality by pressing enter in this file. Finally there is included a transcript of the console window after stepping through the proof, in case you haven't got Coq installed but want to have a look at what this is all about.