Proof Checker
Last updated
Last updated
Before any proof can be verified by a machine, the Math Proof Generation (MPG) process first creates an internal representation of that proof. This representation captures the logical steps that demonstrate a program behaves according to its formal semantics.
While the exact structure of this internal proof representation is still evolving, it is designed with two core principles in mind:
Generic and easy to serialize: The proof should be format-agnostic. That means it can be converted into different machine-verifiable formats like Metamath, Coq, or Lean, depending on the needs of the verifier.
Modular and reusable: Key components of the proof—such as patterns, axioms, sub-proofs, and theories—are designed to be reusable. This means you don't have to reprove them when generating proofs for similar programs.
These properties make it easier to serialize the proof into formats that can be checked efficiently and securely, including in zero-knowledge settings.
In this section, we’ll walk through the two main proof checker formats we currently support: Metamath and a custom format called the block model. We’ll also explain how matching logic and Kore (the intermediate format generated by the K framework) map into each of these proof representations.
is a lightweight language designed to express formal mathematical proofs. Created by Norman Megill in 1990, it was built with minimalism in mind—only 15 basic keywords are used, each prefixed with a $ symbol. This simplicity makes it easy to build and verify proofs, and it’s one reason Metamath is still widely used today.
Because of its minimal syntax, writing a Metamath proof checker is surprisingly straightforward. There are over 20 implementations in different languages, many of which are just a few hundred lines long. This compactness is crucial when deploying checkers inside zkVMs (zero-knowledge virtual machines), where both runtime and footprint matter.
Using Metamath for proof checking in our system means we can either adapt existing proof checkers to run inside zkVMs, or compile the semantics directly into a constraint system for zero-knowledge proofs. Either way, Metamath provides a clean, proven foundation for formal verification.
The block model is a custom proof format we’ve designed from the ground up, specifically optimized for zero-knowledge proof (ZK) systems.
In the block model, a proof is broken down into discrete units called blocks. Each block has a set of input premises and generates a set of conclusions. The rules of inference are hardcoded into the system, so each block must follow these predefined rules.
Here’s how it works:
To construct a proof, a prover provides a series of blocks.
Each block only needs to check that its premises have already been established as conclusions somewhere else in the proof.
Because the order of the blocks doesn’t matter, the proof checking can be parallelized or divided across multiple zkVM circuits.
This “data-parallel” structure is a major performance advantage. Rather than creating a separate SNARK (succinct non-interactive argument of knowledge) for every block, we can generate a single, succinct ZK proof for the entire formal proof. This saves time and computation—especially valuable in environments where efficiency is key.