This implementation of the Metamath Zero kernel is designed for use in the experimental Trivial project. It verifies proofs written in the Metamath Zero binary format and allows introspection of the verifier state/context with basic debugging functionality.
The Trivial Metamath Zero kernel is distributed under the terms of either the MIT license (see LICENSE-MIT) or the Apache License, Version 2.0 (see LICENSE-APACHE).