This is a simple Metamath proof checker developed by Tony Häger. It was packaged and posted to GitHub by David A. Wheeler, with Tony Häger's consent.
It doesn't always print helpful messages when errors are found, and doesn't focus on reporting bad syntax. It is known to compile with GNAT GPL 2015.
The original code was posted on Sun, 16 Jul 2017 20:17:41 +0200
in the posting "Re: [Metamath] Is the turnstile needed?".
The software is released under the GNU GPL version 2 or later (GPL-2.0+), the same license as Norman Megill's Metamath tool.