Overview

If you’ve been around Pi Squared for a while, you must have heard us talking about the K framework. It lies at the heart of our firm belief 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 derive language tools from them. This is illustrated below.

Figure 1: The central vision of the K framework.

The bubble in the center represents the formal definition of a programming language. The smaller outer bubbles it points to represent the tools K produces from this definition, e.g., parser, interpreter, or symbolic deductive verifier.

Any programming language can be given a formal definition, including the opcodes of a virtual machine (VM) or the operations of an instruction set architecture (ISA). 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, once we have the formal semantics of a language, we have everything we need to implement execution tools for that language. Here we mean not only basic tools such as parser, interpreter, or compiler, but also advanced tools such as deductive program verifier or model checker.

While it is theoretically possible to derive these tools for any programming language from its formal semantics, K makes it a reality. Efforts of over two decades led to a scalable framework helping developers to define a language formally and extract a full set of tools automatically.

K has been successfully applied to formalize multiple real-world programming languages, including C, Java, JavaScript, Python, Rust, x86-64, the Ethereum Virtual Machine (EVM), and LLVM IR, making it suitable for both research and commercial applications.

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.