ABCDE: Why we invested in Pi Squared

We believe that Verifiable Computing is a core technology for expanding the computational power and application scenarios of Blockchain in the future. Pi Squared is developing its own unique and effective approach to Verifiable Computing. Supported by world-class engineering and research teams, as well as robust partnerships, Pi Squared will deliver greater efficiency and security for Web3 with its Universal Settlement Layer. It’s for these reasons we chose to support Professor Grigore Roșu and the Pi Squared team from the outset.

Building Scalable Blockchains

Blockchains provide trusted computation without the need for trusted counterparties, ranging from basic token transfers to Turing-complete program functions via a pure P2P network. The most amazing part of blockchain networks is that they’re constructed and run by individuals’ devices, so anyone can participate, and they’re free to leave at any time and join a different blockchain project. Trillions of dollars of assets are successfully owned, transferred, or used as currency by millions of users around the world on such infrastructure today.

Unfortunately, like every cool system, it usually has its own trade-offs. Let’s review the three core features of blockchain networks and those tradeoffs:

1.  Making consensus without trusting any party, but this requires significant computational requirements to achieve consensus.

2.  Communicating via P2P networks, but has a dependence or the limited bandwidth of users (least common denominator)

3.  Infrastructure running on consumer-grade devices, some of which have limited computation and storage capacity.

These characteristics lead to the undeniable fact that on-chain computational resources are truly scarce, which ultimately highlights the downside of blockchain: the performance problem.

The performance issues for blockchains have been one of the central topics of heated discussion over the past few years to the present. Let us bypass the historical retrospection and proceed directly to the conclusion. Currently, the most promising approach to blockchain scalability is the combination of off-chain computation with on-chain verification, or in other words, Verifiable Computing.

With a world-class R&D team^[1]_, Pi-Squared is building Verifiable Computing 2.0, which could position it as a giant in Web3.

The leading tech stack: Proof of Proof

In short, Pi-Squared provides a novel, unique and effective solution based on Mathematical Proofs + Zero-Knowledge Proofs.

Let's start with the basic model of verifiable computing. Typically, there are two roles here, Prover and Verifier; and we use Alice and Bob to represent them respectively.

Assuming Alex wants to prove to Bob that "she knows the solution to 2^30 is 1,073,741,824." In this statement, 2 and 30 are the input values, exponentiation is the relevant operation within the statement, and 1,073,741,824 is the calculation result. So, how can Bob verify that Alice’s statement is correct? Of course, the simplest way is for Bob to directly calculate the result of 2 to the power of 30 according to the given inputs and outputs, following the rules of calculation. Then, by comparing the result he obtained through his own computation with the result provided by Alice, Bob can determine if Alice has made a correct statement. If the result of Bob's own computation matches the one declared by Alice, then Bob can be certain that Alice has informed him of the correct statement.

Let's consider a situation: 1. If Bob is an elementary school student, his computational ability is very limited, and exponentiation is just too complex for him. He does not have the capacity to calculate something as complex as 2^30. So, how can he verify that what Alice says is correct? Or suppose it takes Bob a week, calculating non-stop 24/7, to reach a conclusion, is there any way for Bob to quickly verify and trust that Alice's statement about the computation is correct?

Let's abstract the problem: Is there a solution that allows a computing device with very limited computational power to verify the correctness of a very complex computation result in a short period of time and at a very low computational cost?

Solving this problem has strong practical significance in the field of Crypto. As we mentioned earlier, blockchain networks have very limited computational power, especially compared to the computing devices we use daily, such as smartphones, laptops, and professional computing devices such as servers and large-scale datacenters. Therefore, it is difficult for us to directly perform complex computations on-chain, such as LLM inference and the state settlement of large-scale games. With the increasing recognition of blockchain network limitations, bringing more general and complex computations on-chain has become a very urgent demand. For this reason, over the past few years, researchers and engineers have been exploring relevant solutions to this problem. One of the most feasible technical means to solve this problem is through Verifiable Computing.

We continue to use the example mentioned above to explain the basic implementation principle of Verifiable Computing. To solve the problem between Alice and Bob, we can construct a simple special-purpose machine: the only function of this machine is to verify whether the solution to 2^30 is 1,073,741,824. This machine is divided into two parts, one given to Alice and one to Bob. Alice's part of the machine has three inputs and one output, as shown in the figure below. When we input 2, 30, and x, the machine will make a judgement and return a proof Pi (𝝿).

For Bob's part of the machine, there is only one input: Pi (in actual scenarios, both Pi and the Statement would be sent to Bob, here we have simplified it a bit), as shown in the figure below. If Alice inputs x = 1,073,741,824, then when Bob inputs the Pi provided by Alice, Bob's part of the machine will show “pass”; otherwise, it will show “fail.”

Through this magical machine we've created, Bob can determine whether Alice’s claim about calculating 2^30 is correct without having to compute 2^30 himself.

In the example above, the magical machine we made only deals with a single type of computational verification problem. So, is there a way to extend this magical proof machine to any computation? In other words, for any computational statement proposed by Alice, can the proof generated by our machine allow Bob to verify the correctness of Alice's Statement at an extremely low computational cost?

Magical Proof Machines

The answer is a big yes. Over the past few years, this technology has made significant breakthroughs and has begun to enter the practical application phase. A typical application scenario is zkRollup ^[2]. In the Rollup scenario, the Alice-Bob challenge we need to address is: how to let Layer 1 (L1) verify the correctness of hundreds or even thousands of transactions on Layer 2 (L2) under the execution conditions of a single Transaction.

Most current zkRollup projects, such as Scroll, zkSync, and StarkNet, are based on this pattern, constructing a magical machine known as a zkVM for a specific virtual machine language (VM), for example zkEVM^[3]. This magical component can prove whether the execution of on-chain smart contracts is correct. The zkVM/zkEVM is equivalent to the machine held by Alice, responsible for providing proof for the execution of multiple transactions executed on L2. The contract deployed on L1 is equivalent to the part of the machine held by Bob, responsible for verifying the correctness of the proof provided by the L2 operator. In this way, the L1 can verify the correctness of L2 transactions at a very low computational cost without having to re-run a large number of L2 transactions, thereby alleviating the computational pressure on L1^[3].

At the same time, due to the effectiveness of zkVM/zkEVM in proving Verifiable Computing for complex computations, more companies, such as RISC0, SUCCINCT, Delphinus, are beginning to explore proving more complex computations through this method, such as the complex of programs written in Rust.

However, there is a question here: for Bob, he is shifting trust from his own computations to the proof generated by the magical machine we made. So, is our magical machine really that reliable? The answer is unknown.

Currently, most Verifiable Computing projects are based on low-level machine language-like methods to construct such complex proof machines, such as R1CS, Plonkish, etc. You can search for "how to write ZK circuits" to find them. As the proof capability of the magical machine for computations increases, the more general the computations it can prove, the more complex the ZK circuits required to construct it become. This process is very similar to the making of precision instruments, akin to the production of high-end Swiss watches. Ultimately, the performance and security of the machine largely depend on the programming capabilities of the engineers. Therefore, the auditing of large-scale zkVMs remains a core challenge at present.

The Pi Squared Approach

Pi Squared's novel solution can effectively resolve this predicament. Under the guidance of Professor Grigore Rosu from UIUC ^[4], the Pi Squared team builds upon the open-source K-Framework ^[5], created by Professor Rosu more than 20 years ago, and improved ever since by his UIUC lab and researchers at Runtime Verification and Pi Squared among many others, which provides formal mathematical proofs for programs through the semantics of programming languages. In the field of computer science, formal verification is a method that can mathematically prove the correctness of code.

Thanks to years of research and development, the K-Framework can first be used to construct a Mathematical Proof, and then a small Zero-Knowledge (ZK) circuit can be used to prove the Mathematical Proof. The construction of the Mathematical Proof based on the formal verification of the K-Framework is mathematically demonstrable. The final small-scale circuit for proving the Mathematical Proof is compact, significantly reducing the likelihood of errors in the proof component. In this process, a ZK Proof is generated from a Mathematical Proof. This is also the origin of the project's name, Pi Squared (𝝿2).

Ultimately, through the Universal Settlement Layer (USL) developed by Pi Squared, a broader range of ubiquitous computations, such as proofs of AI programs written in Python, are brought onto the blockchain.

For more information on the technical aspects of Pi Squared and the principles behind the K-Framework, you can refer to the team's official documentation. ^[5][6]

A World-Class team

Prior to founding Pi Squared, Professor Rosu and his team established Runtime Verification. Runtime Verification is an industry-leading formal verification and security company that has provided services to leading Web3 projects and companies, such as the Ethereum Foundation, Uniswap, Lido, Optimism, NASA, and many others ^[7]. The Pi Squared team, led by Professor Rosu and consisting of several former core researchers and engineers from Runtime Verification enriched with fresh talent from UIUC and other top universities, offers fast and efficient verifiable computing services based on years of development.

In addition, Eigenlayer founder Sreeram Kannan (UIUC alum), MegaETH co-founder Yilong Li (UIUC alum), UIUC Professor and renowned cryptography expert Andrew Miller, and University of Pennsylvania Professor and Aleo Founding Scientist Pratyush Mishra serve as advisors for Pi Squared.

Partnership

Through a world-class team of research experts and numerous connections accumulated in the Runtime Verification project and UIUC, Pi Squared has established strong cooperative relationships with projects such as MegaETH and EigenLayer from Day 1. In this round of financing, it was led by Polychain, with investments from multiple institutions including ABCDE, Robot Ventures, Generative Ventures, Samsung Next. The round also included several prominent angel investors such as EF Core Researcher Justin Drake, MegaETH co-founder Yilong Li, Polychain General Partner Karthik Raju, and DAO5 General Partner George Lambeth.

ABCDE and Pi Squared Vision

At ABCDE, we are keen to support projects that are driven by technology to improve efficiencies and reduce costs, and the Pi Squared vision is highly aligned with our investment thesis. We expect that the Pi Squared team's solutions will create real value for the industry.

References

[1] Pi Squared Universal verified computing for all https://pi2.network/team 

[2] An overview of Scroll’s architecture https://scroll.io/blog/architecture 

[3] zkEVM https://scroll.io/blog/zkevm

[4] https://en.wikipedia.org/wiki/Grigore_Ro%C8%99u

[5] K Semantic Framework https://kframework.org/

[6] The Beginner's Guide To Proof Of Proof https://blog.pi2.network/guide-to-proof-of-proof/

[7] Runtime Verification, https://runtimeverification.com/