Matching Logic Proofs Meet Succinct Cryptographic Proofs

This technical report, authored by Bolton Bailey, Xiaohong Chen, Adam Fiedler, Harjasleen Malvai, Andrew Miller, Pratyush Mishra, Nishant Rodrigues, and Grigore Rosu, introduces the foundational research problem that underlies Pi2 Labs's vision for universal verifiable computing. The paper presents the syntax and proof system of matching logic and formulates the research problem of producing succinct cryptographic proofs for checking matching logic proofs -- a concept the authors call Proof of Proof ($\pi^2$). The core insight is deceptively simple yet profoundly consequential: if a zero-knowledge cryptographic circuit can verify the integrity of a mathematical proof, then any computation that can be proved correct using mathematical logic can be verified succinctly and trustlessly. This bridges the gap between the universality of mathematical proofs and the efficiency of cryptographic verification, opening the door to verifiable computing that works for any programming language without requiring language-specific circuits or virtual machines.

The paper begins by presenting the syntax of matching logic in a self-contained manner, making the work accessible to readers from both the formal methods and cryptography communities. Matching logic patterns are built from element variables $x, y, z, \ldots$, set variables $X, Y, Z, \ldots$, and constant symbols $\sigma_1, \sigma_2, \ldots$ using the following constructors: application ($\varphi_1 \; \varphi_2$), bottom ($\bot$), implication ($\varphi_1 \to \varphi_2$), existential quantification ($\exists x . \varphi$), and the least fixpoint operator ($\mu X . \varphi$). From these primitives, standard logical connectives are derived: negation as $\neg \varphi \equiv \varphi \to \bot$, top as $\top \equiv \neg \bot$, disjunction as $\varphi_1 \lor \varphi_2 \equiv \neg \varphi_1 \to \varphi_2$, conjunction as $\varphi_1 \land \varphi_2 \equiv \neg(\neg \varphi_1 \lor \neg \varphi_2)$, universal quantification as $\forall x . \varphi \equiv \neg \exists x . \neg \varphi$, and the greatest fixpoint as $\nu X . \varphi \equiv \neg \mu X . \neg \varphi[\neg X / X]$.

The creation of a zero-knowledge proof of a mathematical proof -- a ZK proof that a math proof was presented and checked -- inspired the name "Pi2 Labs" ($\pi^2$): a cryptographic proof ($\pi$) of a mathematical proof ($\pi$).

The proof system of matching logic is presented as a Hilbert-style deduction system with a compact set of proof rules. These include standard propositional reasoning rules (modus ponens: from $\varphi$ and $\varphi \to \psi$, derive $\psi$, and several tautology schemas), quantifier rules for first-order reasoning (universal generalization: from $\varphi$, derive $\forall x.\, \varphi$; instantiation: from $\forall x.\, \varphi$, derive $\varphi[t/x]$), fixpoint reasoning rules (the Knaster-Tarski rule: from $\varphi[\psi/X] \to \psi$, derive $\mu X.\, \varphi \to \psi$), framing rules (from $\varphi_1 \to \varphi_2$, derive $C[\varphi_1] \to C[\varphi_2]$ for any context $C$) that enable local reasoning similar to separation logic, and rules for the definedness symbol $\lceil \varphi \rceil$ that bridges pattern matching with classical logic. The proof system is sound (all provable patterns are valid) and locally complete (all valid patterns in a given theory are provable from that theory's axioms). A key feature emphasized in the paper is the proof system's minimality: it consists of only about 19 proof rules, making it feasible to implement the proof checker as a very small and auditable program.

The paper explains how programming language semantics can be expressed as matching logic theories. In the K framework, a programming language is defined by its configuration (the structure of program states, including code, environment, store, input/output, etc.) and its rewrite rules (axioms that describe how configurations transform during execution). Each rewrite rule becomes an axiom in the corresponding matching logic theory. Program execution then corresponds to a sequence of rewrite rule applications, and the correctness of an execution -- the claim that a program with a given input produces a specific output -- is a theorem in the matching logic theory. The proof of this theorem is a matching logic derivation that chains together the individual proof steps corresponding to each rewrite rule application.

The central contribution of the paper is the formulation of the Proof of Proof problem: given a matching logic proof (a mathematical proof of program correctness), produce a succinct cryptographic argument (such as a zk-SNARK or zk-STARK) that the proof is valid. The cryptographic argument should be (1) succinct: much smaller than the original proof, ideally constant-size or logarithmic; (2) efficiently verifiable: checkable in time much less than the time to check the original proof; and (3) optionally zero-knowledge: revealing nothing about the proof beyond its validity. The paper argues that this problem is tractable because the matching logic proof checker is extremely simple -- essentially a loop that reads proof steps and checks that each step is a valid application of one of the 19 proof rules. This simplicity translates into a small arithmetic circuit that can be used as the basis for a zk-SNARK or zk-STARK.

$\text{Proof of Proof}: \quad \underbrace{\text{Language Semantics}}_{\text{ML Theory}} + \underbrace{\text{Execution Trace}}_{\text{Proof Hints}} \xrightarrow{\text{Proof Gen}} \underbrace{\text{ML Proof}}_{\text{Math Proof } \pi} \xrightarrow{\text{ZK Circuit}} \underbrace{\text{Cryptographic Proof}}_{\pi^2}$

The paper discusses the architecture of the Proof of Proof system. The process begins with a program execution (or verification task) that produces proof hints -- annotations that record which rewrite rules were applied and how. These hints are consumed by a proof generation engine that constructs the full matching logic proof. The proof is then fed into a proof checker circuit -- a ZK-compatible arithmetic circuit that implements the matching logic proof checking algorithm. The circuit produces a succinct cryptographic proof that the matching logic proof is valid. The block model is introduced as a custom proof format optimized for zero-knowledge proof systems, where a proof is broken down into discrete units called blocks, each with a set of input premises and generated conclusions, with rules of inference hardcoded into the system. This block-based representation enables efficient parallelization and pipelining of the proof checking process within the ZK circuit.

The paper highlights the universality of the Proof of Proof approach as its most distinctive advantage over existing verifiable computing solutions. Traditional approaches to verifiable computing, such as zkEVMs, are tied to a specific virtual machine or instruction set architecture. If a computation is written in a language that does not compile to the supported VM, it cannot be verified. In contrast, Proof of Proof works for any programming language whose formal semantics has been defined -- including C, Java, JavaScript, Python, Solidity, the EVM, RISC-V, and any future language. No compilation or translation to an intermediate representation is required; the program is executed in its native semantics, and the proof is generated directly from that execution. This universality comes from the fact that matching logic is a general-purpose logic capable of expressing the semantics of any programming language, and the proof checker circuit is language-independent.

The practical implications of Proof of Proof are discussed in the context of blockchain and decentralized computing. In the blockchain setting, verifiable computing is essential for scaling: layer-2 solutions (rollups) execute transactions off-chain and produce proofs that the execution was correct. Current zkRollup solutions are limited to specific VMs (typically the EVM), but Proof of Proof enables rollups for any programming language or VM. The paper also discusses applications to cross-chain interoperability (proving that a transaction was correctly executed on one chain to another chain), smart contract verification (proving that a smart contract satisfies its specification), and trustless oracles (proving that an off-chain computation produced a correct result). The trust base is optimally minimal, consisting of only the formal semantics and the matching logic proof checker circuit.

In conclusion, this technical report lays the intellectual foundation for a new paradigm in verifiable computing. By combining the universality and expressiveness of matching logic with the efficiency and trustlessness of succinct cryptographic proofs, the Proof of Proof concept transcends the limitations of VM-specific approaches and offers a path to truly universal verifiable computing. The paper's contributions include a clear presentation of matching logic's syntax and proof system, the formulation of the Proof of Proof problem, and a discussion of the architectural considerations for implementing the system. The work represents a convergence of decades of research in formal methods, programming language theory, and cryptography, and serves as the theoretical cornerstone of Pi2 Labs's mission to make verifiable computing accessible for all programming languages and applications.