It's a poorly named metamath verifier - View it on GitHub