BYOL (Bring Your Own Language) to Web3

In the evolution of Web3, we’ve seen a steady increase in developer openness and a better developer experience. Initially, Ethereum developers were limited to coding in Solidity. Today, the landscape has expanded to include languages like Rust, WASM, and Move, with the variety of languages and virtual machines (VMs) continuing to grow.

Pi Squared is advancing this evolution by driving the Web3 ecosystem toward a truly ‘VM agnostic’ future. Pi Squared’s goal is to empower developers to write secure, verifiable programs in any language, VM, or zkVM. Pi Squared envisions a future where millions of verifiable programs run asynchronously, all seamlessly interoperating through a ‘Universal Settlement Layer.’

What sets Pi Squared apart is its use of an innovative mathematical proof design known as ‘Proof of Proof.’ Here’s a brief overview of how it works:

1. A mathematical proof of execution is generated.
2. This proof is then input into a cryptographic system, producing a zero-knowledge (ZK) proof that certifies the correctness of the mathematical proof.
3. Finally, any smart contract can verify this ZK-proof certificate through a simple circuit.

In this article, we delve into the K Framework, a critical tool for generating these mathematical proofs. We’ll explore the advantages that mathematical proofs offer developers, and discuss how this technology is poised to drive the future of Web3.

K Framework

The K framework is a formal framework for defining programming languages and analyzing programs written in those languages. It was created by Pi Squared CEO Grigore Rosu in 2003 and developed and refined over years of work in both academia and industry. The value of K has been proven by practical deployment in the industry at Grigore's first company, Runtime Verification, which has used K to verify the correctness of smart contracts and other software systems. The core logical framework of K is *matching logic*, a minimalistic but expressive and versatile logical framework that captures other logical frameworks used in language semantics and program analysis as theories (i.e., sets of matching logic axioms, or patterns). Any mathematical statement, in particular the result of a program execution, can be expressed in matching logic as a theorem, and the K framework provides an automatic and efficient way to formulate such theorem statements about the programs written in a given programming language and extract a mathematical proof of it constructively, from the program execution itself. Matching logic can capture any mathematical statements, but we here limit ourselves to statements corresponding to program execution — but in arbitrary programming or VM languages.

Pi Squared uses matching logic to prove statements about execution traces and other aspects of programs. This approach has a few benefits. Dealing with the mathematical representations of these programs allows us to bring any programming language into the same proof system. Mathematical proofs have capabilities that naive (cryptographic) proofs of execution do not. For example, mathematical proofs can encode arguments about optimisations to a base program that allows its execution to be proved faster. Mathematical proofs have the potential to prove things beyond execution. Through techniques like formal verification, we have the potential to put proofs of security properties for smart contracts onto the chain. The key innovation above and beyond all of these is that Pi Squared uses ZK proofs to make these proofs as efficient as possible, simultaneously achieving expressivity and efficiency.

BYOL (Bring Your Own Language)

If you’re a developer looking to use a specific language, like Rust, integrating with Pi Squared is straightforward. To get started, you’ll need a description of Rust’s semantics—or those of a lower-level language that Rust compiles to—within the K Framework. Once these semantics are specified, you can create a proof-of-proof that verifies the execution of your Rust program. This is the same process for turning any VM into a zkVM!

At launch, Pi Squared plans to support several zkVMs as backends for Pi Squared, that is, as ZK proof generators for the correctness of matching logic proofs. If you’re developing on one of these supported zkVMs, integrating with Pi Squared could be as simple as replacing your program’s cryptographic commitment with our proof-of-proof system’s commitment.

Using your program with Pi Squared offers numerous benefits, primarily centered around two key advantages:

1. Succinct Verification: With Pi Squared, you no longer need to rely on a centralized server or operator to ensure your program has run correctly. The ‘Proof of Proof’ system allows you to continue using your preferred programming language while also verifying the program’s execution. Because this verification is based on a zero-knowledge (ZK) proof, it is both succinct and efficient, enabling almost instant verification. This capability also enhances interoperability between different programs via the Universal Settlement Layer, which we’ll discuss further later.
2. Enhanced Security: In addition to ensuring correct execution, the K Framework seamlessly provides formal verification capabilities which are also language-parametric and can be instantiated with any programming language or VM. Although not enforced to prove correct execution, formal verification helps users prove much more complex properties of their programs, such as conformance with requirements specifications, functional correctness, and the security of the programs they interact with.  All these can then be incorporated in the final ZK proof, which thus guarantees not only the correct execution of a program according to its language semantics but also the correctness of the program itself that produced that execution concerning its formally verified properties. Moreover, it establishes a new standard for multi-language support and interoperability, based on language semantics rather than ad-hoc aggregations of multiple VMs. By reducing the risk of hacks and cross-domain vulnerabilities, Pi Squared minimises potential security breaches and cross-platform damage.

A Million Verifiable Programs

Pi Squared envisions a future where Pi Squared programs challenge the centralized nature of Web2, empowering users with greater sovereignty and control. Imagine a world with millions of programs running simultaneously, all seamlessly producing Pi2 proofs and interoperating. To support this vision, a scalable and minimal base layer is essential—one that serves as the ultimate source of truth. This is where the ‘Universal Settlement Layer’ comes in. As one of the first projects built on Pi Squared’s technology, it provides a unified, minimal base layer optimized for Proof of Proof verification across multiple programs.

If you're a developer, ZK project or just curious to learn more about Pi Squared, we would love to chat! Feel free to reach out at contact@pi2.network.