MEPK: a Minimal Extensible Proof Kernel

Author: Marnix Klooster marnix.klooster@gmail.com

License: GPLv3

This is a Java library for building checked Metamath/Ghilbert-like proofs, which should be sufficient for verifying all Ghilbert and most Metamath proofs.

Building

MEPK is a standard Maven project. To compile, run the tests, and install the jar into your local repository:

mvn clean install

To only compile and run the tests:

mvn clean test

Requirements:

• JDK 17 or newer to build. The build uses maven.compiler.release=17, so it always produces Java 17 class files (bytecode major version 61) no matter which JDK compiles it — the resulting jar runs on Java 17 or newer. Because release also restricts the compile-time API to Java 17, building on a newer JDK cannot accidentally pull in newer-than-17 APIs.
• Maven 3.6+ (any recent Maven 3). All build plugins are pinned in pom.xml, so the build is reproducible on any Maven-supported platform (verified on Linux and Windows).

API documentation can be generated locally with:

mvn javadoc:javadoc

Continuous integration runs on GitHub Actions (.github/workflows/ci.yml): every pushed commit and pull request runs mvn clean verify site on JDK 17 using the runner image's bundled Maven (documented as Maven 3.9.16 / JDK 17.0.20 in the current ubuntu-24.04 image); each run logs the exact versions via mvn -version. The site step generates the Javadoc, so a Javadoc error fails the build. For the latest commit on the default branch, that already-generated Javadoc is published to GitHub Pages at https://marnix.github.io/MEPK/ (the deploy job does no Maven work). (Build outputs are not distributed; see the "distribute binaries?" to-do below.)

To-do list for functionality:

• Design and implement abbreviations. My current best design idea is the following.

  (TODO: Try and generalize or replace the idea below by using the concept of 'profiles'. See my "Using 'profiles' for conservative extension / definition mechanism" mail to the Metamath mailing list.)

  • We do not introduce a new 'abbreviation' proof step.

  • Every proof has a set of abbreviations AA, so that a proof means, "From grounding statements SS-after-expanding- all-of-AA one can construct statements TT-after-expanding- all-of-AA, using only proof steps."

    Rationale. We also expand AA in the grounding statements SS, since I've seen a case which I very much would like to work, for which I see no other solution. (TODO: Add succinct description of such a use case.) I don't see any downside to this expansion of SS. The alternatives are to forbid AA in SS, or not expand AA in SS, so that there would be no valid proof using an abbreviation A where SS uses A. But that does not seem to solve any problem.

  • When verifying that a proof really proves statement T, it shows how to construct T-after-expanding-all-of-AA.

  • Abbreviation introduction is by a (non-kernel) proof which is created from a statement T and an abbreviation A: this proof grounds only T; has A as its sole abbreviation; and its only grounding statement is T-after-expanding-A.

  • Abbreviation elimination is by a (non-kernel) proof which is created from a proof P (with grounding SS and grounded TT) which has abbreviations A and AA: the created proof has grounding statements SS; its grounded statements are TT-after-expanding-A; and it has only abbreviations AA.

  • An abbreviation can also add hypotheses, so that it is possible to say, "(group-elem x) abbreviates (Real x) for which (> x (0))".

  Rationale. The key property for an abbreviation mechanism, and in general for any definition mechanism, is that an abbreviation should not allow new statements to be proved. To be more precise, if we can construct T from SS using abbreviation A, where this abbreviation is not used in T, then it must also be possible to construct T from SS without using abbreviation A.

  The above idea makes sure that this property is checked by our proof verification algorithm: the only part that will be built in is the expansion of an abbreviation.

  Implementation idea for verification of abbreviations:

  • Create mepk.kernel.util.ExpandedAbbreviationsProof which is a wrapper around an arbitrary proof. This expands all the wrapped proof's abbreviations (in the grounded statements and in its justification ProofStep), and wraps the justification Proof again in a NoAbbreviationsProof.

  • Proof#verify() then wraps itself in this way, and verifies the result using the current verification algorithm.

  An alternative is to introduce an 'abbreviation' proof step. That would make our verification algorithm simpler, but it makes it impossible to check the key property.

  Note: Using an abbreviation elimination proof, a proof "the positive reals form a group" can be used to translate statements about a group into statements about the positive reals.

  Open issue: Can these features be used to create a proof "the positive reals form a group"? I think they can: it should be possible to create a proof based on the real number theorems, with abbreviations "(group-elem x) abbreviates (Real x) for which (> x (0))" and "(op x y) abbreviates (* x y)", of a statement like

  (group-elem x) AND (group-elem y) ==> (group-elem (op x y))

  which expands to the two (!) statements

  (Real x) AND (> x (0)) AND (Real y) AND (> y (0)) ==> (Real (* x y))

  and

  (Real x) AND (> x (0)) AND (Real y) AND (> y (0)) ==> (> (* x y) (0))

• Perhaps implement export based on a proof's justifications (getJustificationFor())? Idea for a format:

  • Stack-based like Metamath's;
  • For each of getGrounded(), first output (the used part of) the Justification's Proof followed by its ProofStep;
  • Every part is output on a separate line, with a prefix HYP for the 'null' justifications, and prefixes COMPOSE, SUBSTITUTE, WEAKEN for the proof steps;
  • Compressed in BZip2 format (since the above has a lot of duplication).

Implementation issues:

• Enforce a standard code format in the build. The sources are hand-formatted to a consistent style, but nothing checks it, so the formatting drifts. Add a standard formatter as a build step that verifies rather than rewrites, so a commit which does not match the format fails the build instead of being fixed silently. Candidates, in order of preference:

  • maven-checkstyle-plugin with a standard ruleset (google_checks.xml or sun_checks.xml), bound to a lifecycle phase and configured to fail on warnings.
  • net.revelc.code.formatter:formatter-maven-plugin, or spotless-maven-plugin with google-java-format, in check mode, for an exact canonical format rather than a ruleset. NB before picking one: all sources are indented with TABs, and both standard rulesets flag tab characters, so switching to either means reformatting every file in the project (23 violations across 36 files for the tab check alone). Decide first whether to reformat the code to spaces in one dedicated commit, or to keep tabs and write a small project ruleset that permits them -- the latter is much less churn. Either way, add the config to the repository so the rule is explicit and reviewable, and pin the plugin version as the rest are. Independently of the formatter, consider enabling -Xlint:all in maven-compiler-plugin so javac warnings are visible; CI currently reports neither.

• Make the Javadoc build fail on warnings, not only on errors. (Verified: a bad {@link} on a public member does fail mvn site, so the CI comment and the "Building" section above are accurate as far as errors go. But a javadoc warning -- e.g. a duplicate @return tag, or a missing one -- is only logged and the build still succeeds.) Add <doclint>all</doclint> and failOnWarnings to the javadoc configuration, so documentation quality is enforced like the rest of the build. Note the plugin's default only documents public/protected members, which is the right default here.

• Change method names so that every Set is called a 'theory', e.g., getGrounding() -> getGroundingTheory()? Con: The current names are short, and that is good. For now I'll keep the current behavior.

• Group / rename the test files. Names like Test1 are uninformative and the tests are split by incidental history rather than by what they cover. Reorganize by kernel component / concern (e.g. substitution, compose, weaken, DVRs, parser, abbreviations) with descriptive class names. (Started: TestSubstitution and TestVerify now cover substitution/DVR interaction and verify()'s rejections respectively. Test1 and TestCompose still to do.)

• TrustedProof name/function mismatch. The class is named "Trusted" but is actually the untrusted composition layer built on top of mepk.kernel (it adds no primitive inference; its outputs are re-checkable by the kernel's verify()). It lives in mepk.builtin on purpose (see commit 5a9a110 "kernel split off": once ProofStep became a Proof, TrustedProof was pure composition). Two fixes:

  • Rename it to a DSL-ish name (e.g. Proofs or ProofBuilder) so the name reflects "convenience constructor", not "trust boundary".
  • Move the trust-establishing verify() call OUT of its constructor (added in commit a1a8ff5, and only under -ea; see soundness list below). A non-kernel class should not be the thing that (conditionally) decides trust.

Kernel correctness / soundness to-do (found in a 2026 audit; do the soundness items BEFORE any hashing/signing/serialization work — they are ordered by severity):

• S3/S4 (downgraded: believed unreachable). S3 was that the DVRSet symmetry invariant is only checked under -ea, and S4 that andDistinct(DVRSet) does not symmetrise its input. On closer inspection both look unreachable: the DVRSet(Map) constructor is private, and every public way of building a DVRSet (Distinct(...), andDistinct(...), substitute) preserves symmetry, so an asymmetric map cannot be injected from outside the class. The -ea-gated check is therefore redundant belt-and-braces rather than a soundness hole. Worth confirming with a test that pins the symmetry invariant, so that it stays true if the class is ever refactored, but it should not block other work.

• Capture on substitution (not yet decided). Substituting x := (f z) into a statement that separately mentions z reuses a variable that is already in play, and is accepted. The related case of reusing a variable that x is already DISTINCT from is rejected ("may not be disjoint with itself"), so the code clearly cares about variable collisions; this is the same class of problem, one case over. DECIDE: reject the substitution, rename to a fresh variable, or allow it. Note that requiring the variables of a replacement to be pairwise distinct from each other would be WRONG: a multi-variable replacement legitimately hands one variable's role to several variables, and Test1.testSubstituteInDistinctVariables pins that behaviour deliberately (x := (+ x1 x2) into DISTINCT (x y) yields DISTINCT (x1 y) and DISTINCT (x2 y)).

• verify() is only CALLED under -ea. TrustedProof's constructor gates the verify() call behind the assertion trick, so by default (JVM assertions off) proofs are constructed and never verified. Either make verification unconditional, or -- better -- keep the rule constructors as the soundness mechanism (they already enforce substitution/DVR legality) and let verify() be a redundant, independent cross-check that always runs in CI. NB: verify() currently only checks the wiring between steps and trusts each ProofStep's getGrounded1(), so the per-step legality checks must remain in the rule constructors regardless.

• ExpandedAbbreviationsProof is a no-op stub (getGrounded() / getJustificationFor() have // TODO: ...with all abbreviations expanded), yet it runs inside the TCB as verify()'s abbreviation-expansion step. Until it truly expands, abbreviations are not soundly handled (the getAbbreviations().isEmpty() guard papers over this). Soundness-relevant because abbreviation conservativity is a TCB concern.

• Justification is half-checked and half-immutable: its proofStep/proof fields are non-final (unlike Statement/Expression/DVRSet), and its prerequisite check is an assert. Make the fields final, and promote the check to a thrown MEPKException so the failure is the documented MEPKVerificationException in every configuration rather than an AssertionError thrown out of a constructor. Worth being precise about what this is worth, because it is not a soundness hole. The assert is redundant, not load-bearing: verifyStatementsAreJustified re-tests the identical condition and throws on it ("does not prove everything that is required"). Measured both ways -- with assertions off the bad justification constructs silently and verify() rejects it; with -ea the constructor throws first and verify() is never reached. Either way it is rejected, which is what TestVerify.rejectsAnInsufficientSubProof pins. So an incorrect justification yields a bad data structure, not a false theorem; it can only matter if a caller treats getGrounded() as proven without calling verify(), which brings us back to the -ea gate above as the real exposure in this area. This item is about consistent, diagnosable failure. NB: final is not a tamper-resistance measure. A private non-static field is reflectively writable whether or not it is declared final (both verified), so final buys safe publication, compile-time enforcement inside the TCB, and consistency with the other value types -- and nothing more.

• Var and App are not final (unlike the other kernel value types), and App's constructor stores the Expression[] without a defensive copy -- a minor immutability leak inside the TCB. Make them final and copy the array on construction.

• verify() is recursive with an acknowledged JVM-stack-depth risk on deep proofs; convert to an explicit iterative worklist before running large corpora (e.g. set.mm).

• Assurance (not a bug, but needed to trust the above): add a second, independent verifier as a differential cross-check on set.mm (candidate: the author's marnix/zigmmverify, or checkmm); fuzz the parser (which is outside the TCB, so parser bugs yield wrong/malformed statements, never false theorems).

• Distribute binaries? Currently no need — CI does not keep build outputs. If a need arises, decide how: e.g. split the trusted kernel (mepk.kernel) into its own jar separate from mepk.builtin (parsers/DSL), so consumers can depend on just the TCB; and/or publish to Maven Central (which would also enable free Javadoc hosting via javadoc.io).

• Mark versioned releases (low priority; prerequisite for the above and for javadoc.io): tag releases and drop the -SNAPSHOT for a released version.

• Migrate tests JUnit 4 -> JUnit 5 (Jupiter). The tests use JUnit 4.13.2, which is the newest JUnit 4 but effectively frozen: 4.13.2 (Feb 2021) is the last release and JUnit 4 gets only rare critical fixes — active development is entirely on JUnit 5, which is the current industry standard (default in Spring Boot, build-tool archetypes, and IDE wizards). Not urgent (4.13.2 is stable, and JUnit 5's Vintage engine can even run JUnit 4 tests as-is), but worth modernizing. This is a real API change, not cosmetic: swap the dependency for org.junit.jupiter:junit-jupiter (test scope), then update the 5 test classes — @Before -> @BeforeEach, @Ignore -> @Disabled, org.junit.Test/Assert -> org.junit.jupiter.api.Test/Assertions. Surefire 3.x (already pinned) runs Jupiter natively. The suite is small (5 classes), so the migration is low-risk. Consider OpenRewrite's JUnit4->5 recipe to automate it.

• (Optional) Further trim CI build time. Caching now works: a warm run (unchanged pom.xml, so the ~/.m2 cache is restored) does the seed in ~3 s and the build in ~11 s, down from ~30 s cold — the Maven cache-seed step in .github/workflows/ci.yml ensures the saved cache is complete (see that step's comment for why). Only remaining idea, if a run is ever still slow: trim plugins pulled in by site (e.g. project-info reports) when only Javadoc is needed.