Overview

If you’ve been around Pi Squared for a while, you will hear about us talking about the K framework. It lies at the heart of our firm believe and persistent pursue of correctness: correctness of programs and programming tools. In this guide, we break it down for you.

K is a language framework. It allows people to write formal definitions of programming languages and automatically derived language tools. This is illustrated as below.

Figure 1: The central vision of the K framework.

The bubble in the center represents the formal definition of a programming language.

Any programming language can be given a formal definition, including the OpCodes of a virtual machine and the operations of an instruction set architecture. The formal language definition, sometimes also referred to as a formal semantics of the language, is a complete and rigorous mathematical definition of the behaviors of all programs of that language.

Therefore, in theory and in principle, once we have a formal semantics of a language, we have everything we need to know to implement tools of that language. Any tools. Not only basic tools such as a parser, an interpreter, and a compiler, but also advanced tools such as a deductive program verifier and a model checker. The formal semantics of a language has all the information one needs to develop all these tools of the language.

It is theoretically possible to automatically derived all the above-mentioned language tools for any programming language from its formal semantics, but K makes it a reality.

In the past two decades, K has been through several major revisions and re-implementations and has incorporated with numerous novel technological innovations and engineering optimizations.

As of today, K has been successfully applied to completely define the formal semantics of large programming languages, including C, Java, JavaScript, Python, Rust, x86-64, the Ethereum Virtual Machine (EVM), and LLVM IR. K is scalable and practical. It works.

At Pi Squared, we use K at two different levels:

Correct-by-Construction Computing (K as a Prover)

We use K to execute programs directly based on the formal semantics of the programming language, reducing the need for manually implementing any language-specific interpreters or compilers and thus avoiding their bugs.

Program execution is correct by construction, meaning that the execution results obtaining from K is automatically correct modulo the correctness of K itself and the formal semantics of the language.

Verifiable Computing (K as a Proof Searcher)

We use K as an intermediate step to generate machine-checkable mathematical and zero-knowledge proofs (ZKPs) of program execution, directly based on the formal semantics of the programming language, which further eliminates K from the trust base.