Matching Logic

Matching logic is the foundation of the Proof of Proof framework. It provides a unified way to define and reason about the semantics of any programming language using mathematical logic.

In matching logic, a programming language is described as PL math theory, which is a structured collection of axioms that define how programs behave. This logical structure makes it possible to reason about execution, correctness, and equivalence in a precise and formal way.

Why Matching Logic?

Matching logic is both expressive and minimal:

• It’s expressive enough to describe any programming language or computational model—imperative, functional, object-oriented, or otherwise.

• Despite this expressiveness, it supports the smallest known proof checker—just 200 lines of code. That’s all it takes to verify any program execution written in matching logic, making it ideal for integration with systems like zkVMs and ZKPs.

Thanks to the K framework, many major programming languages have already been formally defined using matching logic, including: C, Java, JavaScript, etc.

These definitions are more than theoretical—they're used to build tools like interpreters, model checkers, symbolic execution engines, and program verifiers. K turns formal definitions into executable implementations.

Matching Logic Syntax

Matching logic uses a small set of constructs to express powerful logical patterns:

φ ::= x | X | σ φ₁ … φₙ | ⊥ | φ₁ → φ₂ | ∃x.φ | μX.φ   (if X is positive in φ)

These expressions, called patterns, can match a wide range of structures—from simple terms to full program states.

Below is an explanation of what each component means:

• x: Element variables, like those in first-order logic (FOL), used to refer to individual elements.

• X: Set variables, similar to propositional variables in modal logic, used for predicates or sets of elements.

• σ φ₁ … φₙ: Constant symbols applied to sub-patterns. These represent functions, predicates, constructors, or even program states.

• ⊥: The bottom value, representing contradiction.

• φ₁ → φ₂: Implication.

• ∃x.φ: Existential quantifier, expressing that some value makes φ true.

• μX.φ: Least fixpoint, used to express recursive or iterative properties (e.g., loops or reachability).

What Patterns Capture

Patterns are the core building blocks of matching logic. They allow us to:

• Match data structures with specific shapes

• Describe valid transitions between program states

• Capture dynamic behaviors and constraints over time

In practice, this makes matching logic suitable for both low-level reasoning (e.g., arithmetic correctness) and high-level semantics (e.g., verifying smart contracts or system invariants).