# Overview *If you’ve been around Pi**2** Labs 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.
The central vision of the K framework

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 several real-world programming languages, including [C](https://pi2.network/papers/defining-undefinedness-of-c), [Java](https://pi2.network/papers/k-java), [JavaScript](https://pi2.network/papers/kjs), [Python](https://pi2.network/papers/python-semantics), [Rust](https://github.com/runtimeverification/mir-semantics), [x86-64,](https://pi2.network/papers/formal-semantics-x86-64) [the Ethereum Virtual Machine (EVM)](https://pi2.network/papers/kevm), and [LLVM IR](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.7), making it suitable for both research and commercial applications. At Pi2 Labs, 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. --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.fast.xyz/k-framework-archived/overview.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.