Matching logic and mathematical proofs of program execution

Pi Squared uses matching logic and the K framework to mathematically prove that program executions are correct, enabling trustworthy and language-agnostic development tools.

When you write code, it's usually pretty simple: you pick a language, type your program, and use tools like compilers or interpreters to make it run. That's the normal deal, and sometimes programmers simply take these tools for granted. 

But there's a catch. What if those tools get it wrong? What if they have bugs? And actually, they most likely do have bugs because these tools are built from complicated software, sometimes with millions of lines of code. If something’s off in how these tools are built or how they process your program, it could go haywire.

The people building these compilers and interpreters want them to be bulletproof, but proving every part works perfectly is nearly impossible. And that's a trust problem.

At Pi Squared, we're not trying to prove the whole system's perfect, but we are trying to prove that each job it does is right. We do this by using an approach called matching logic. It's a way to formally, mathematically, and rigorously define the behaviors of any program in any programming language using finitely many semantic rules. Instead of writing code, we write these rules that say how code should work. These rules are like a blueprint for the language, and they're the key to building tools that you can trust.

In this post, we’ll walk you through how matching logic and the K framework team up to prove programs run the way they should. You’ll see how we define a language’s rules, build tools from them, and use math to check every step.

What are Semantics?

Semantics defines the meaning of your code—what it actually does when it runs, not just how it’s written. While syntax is the structure, semantics is the behavior. A semantics of a programming language defines the behaviors of all programs written in that language, rigorously and mathematically. At Pi Squared, we use matching logic to define the semantics of any programming language. This lets us prove each job, like running code, is correct, and this capacity has been baked into the K framework.

Watch our ETHDenver 2025 session below to learn more.

The K Framework: Building tools from rules

The K framework is a tool that takes the rules of a programming language and builds tools from them. These tools can be anything from parsers that read your code to interpreters that run it. Instead of writing these tools yourself, the K framework creates them automatically based on the formal semantics. You just define how the language works — things like what a loop does or how variables get assigned — and K handles the rest.

The K framework is at the heart of what we do at Pi Squared. It lets us define the semantics of a language in a formal way and then use those semantics to automatically generate tools that run programs.

Figure 1: The K framework generating tools to run programs 

It has generated tools for C and Java, for example, straight from their semantics in a fully automatic way. This way, we can separate the design of a language from the tools that make it work. Language designers can focus on making a language that's easy to use, and K takes care of the hard part of building tools that run it.

Matching logic

Matching logic is a way to turn the correctness of program execution into proving math theorems. It takes the semantics of a language and describes what's supposed to happen when you run your code. We use matching logic to write down exactly how a program should work in a clear, logical way. It's the foundation of how K understands languages — it lets us take the rules we defined and describe what's supposed to happen when you run your code.

Here's how it works. When you write a program, you're telling the computer to do something. You're giving it a set of instructions, and you expect it to follow them. Matching logic lets us write down these instructions in a formal way. We can say things like, "If you see this, then do that," or "This should happen before that." These rules are like a blueprint for how a program should run, and they're the key to proving that a program does what it's supposed to.

Proving it works

At Pi Squared, we don't try to prove the whole K framework is perfect—that's next to impossible with over half a million lines of code that's always changing. Instead, we focus on each thing it does, like running your program or checking if it's correct. For every task, we use matching logic to create a proof—a mathematical way to show that this one job went exactly as planned.

When K runs your code, it keeps track of every step—where it starts, what rules it follows, and where it lands. Matching logic takes that and turns it into a formula we can prove, like saying, "This program starts here and ends there, and every move in between checks out."

These proofs are like certificates—you can look at them and know they're legit. We tested it with a simple program that ran 100 steps, and it made a huge proof, 1.6 million lines long, but our checker confirmed it in just 5.6 seconds. That speed matters—it shows this isn't just theory; it can work for real.

This is how we were able to achieve this. First, K gives us what we call proof parameters—a log of what it did, like the exact steps and rules it used. Then we take that log and turn it into a full proof with matching logic. After that, we hand it to a matching logic proof checker, a small, fast tool that double-checks everything.

We trust this matching logic proof checker because it's simple and solid—perfect for catching mistakes. Some parts of these proofs, like the basic logic rules, only need to be checked once and can be reused. The rest, tied to your specific program or language, gets built fresh each time. It's a smart way to skip wrestling with all of K and just nail down what's happening right now. 

Wrapping it up

We’ve walked you through how we use matching logic and the K framework to prove programs work the way they’re supposed to. It starts with semantics—defining what code really means—then moves to building tools from those rules with K.

Matching logic turns that into math we can prove, step by step, so you know every job, like running a program, is solid. It’s all about trusting tools that are fast, reliable, and work for any language, right from the ground up. That’s what we’re doing at Pi Squared.

Want to know more? Our whitepapers provide deep insights into all the parts of our technology. For a simpler breakdown, check out our docs — they'll give you the big picture without the heavy details. If you want to join our developer community, you can sign up on our developer portal.