Package mepk
It is a proof kernel, i.e., a trusted core to create Java objects representing mathematical proofs. It is minimal in the sense that all valid proofs can be created using this core alone. It is extensible, so that it is possible (probably for reasons of performance) to create the same proofs through new mechanisms.
The trusted kernel is the mepk.kernel package (with its subpackages):
all other proofs, including those in mepk.builtin, are built on top of that kernel, and
each proof can be verified using Proof.verify().
The mepk.builtin package contains some basic proofs and proof combinators.
The main entry point is TrustedProof.
The code was carefully designed to make sure that Proof.verify()
always succeeds for a TrustedProof;
but in case of doubt you can always verify() that.