 Juha Arpiainen has implemented his own proof checker in Common Lisp called Bourbaki and Marnix Klooster has coded a proof checker in Haskell called "Hmm".Although they all use the overall Metamath approach to formal system checker coding, they also implement new concepts of their own.Mel O'Cat designed a system called "Mmj2", which provides a graphic user interface for proof entry.