Skip to main content

· 7 min read
Victor Graf

Where’s Waldo is a favorite analogy for zero-knowledge proofs. In particular, if you want to prove you know where Waldo is, without revealing his location, you can:

  1. Have your friend, the verifier, print a Where’s Waldo puzzle on a big poster board.
  2. Take the poster board, turn around and cut out Waldo from the image. Dispose of the rest.
  3. Hand the cut out of Waldo to your friend, who makes sure it’s really Waldo.

This is kind of like a zero-knowledge proof (with less cryptography and more craft supplies), but why not implement a real zero-knowledge proof to show you know where Waldo is?

This example implements a RISC Zero program which allows a prover to convince a verifier they know Waldo’s location in a public Where’s Waldo puzzle, without revealing Waldo’s coordinates.

To get a better understanding, browse the source code and run the example yourself.

Overview​

This example of implementing a proof for Where’s Waldo is designed to help you understand some useful techniques in creating more advanced programs with RISC Zero.

In particular, it should help you understand:

  • Merkleizing large data to give the guest verifiable access to small parts of it.
  • Using external libraries in the guest to avoid reinventing the wheel.

This tutorial will not include:

Implementing Where’s Waldo​

The approach for this example is similar to the analogy. It takes the full Where's Waldo puzzle image and “cuts out” just Waldo.

This cutting out operation takes place in the zkVM guest which keeps the inputs, and in particular Waldo’s coordinates, private while allowing the verifier to confirm that computation was done correctly. In this case, the guest’s journal includes a commitment to the Where’s Waldo puzzle image and the cut out image of Waldo.

Once the verifier has checked the receipt and the source image commitment in the journal, and given the cut out image a look to verify it really is Waldo, they can be sure that Prover knows where Waldo is in the puzzle.

Key to this procedure is that the verifier checks that the Prover did not cut Waldo out of some other source image than the verifier was expecting (e.g. that they didn't go and cut Waldo out of a different puzzle because they don’t actually know where Waldo is in the puzzle the verifier gave them). This is a common problem when implementing verifiable programs, and this is what the source image commitment handles in this example.

Now let’s talk about one strategy to tackle this problem, especially for large data such as images, Merkleization.

Merkleization​

In the simplest approach, the guest program could create a commitment simply by hashing the whole Where’s Waldo image in memory and use the hash as a commitment. Unfortunately, hashing the whole image, which we expect to be rather large, is cost prohibitive in the guest. So how can the guest access the data it needs without giving the host an opportunity to give it inconsistent data (e.g. swapping out the Where’s Waldo puzzle)?

Because we only need access to a relatively small portion of the image to produce the cutout, a viable approach is to split the image into a vector of small image chunks and use a Merkle tree to commit to this vector. As needed, the zkVM guest can then ask the host chunks of the image, and along with each chunk the host can provide a Merkle path that proves the chunk is part of the committed image. This gives the guest access to the data it needs, while ensuring it is all part of the committed image.

Merkle trees are an example of a vector commitment. Given a Merkle root, which is simply a SHA-256 digest, the guest has a commitment from the prover binding it to the full data vector. In particular, the guest can then send a request to the host for a specific element in the full vector, and the host will respond with the data and a Merkle path. With this Merkle path, which is a short chain of hashes leading back to the root, the guest can verify the data came from the committed vector. This is great because it means the host can commit to very large data vectors, on the order of gigabytes or even terabytes, and the guest can access small portions of it on demand without reading the whole thing. This trick, of having the prover commit to a large amount of data then the verifier reading a small portion, is actually at the core of the RISC Zero zero-knowledge proof.

In the Where's Waldo example, the data we want to Merkleize is the source Where's Waldo puzzle image. In order to turn it into a vector, we cut the image up into chunks and the give each an one-dimensional index. E.g. an image split into four chunks could be numbered 0 as the top-left quadrant, 1 as the top-right, 2 as the bottom-left, and 3 as the bottom-right. This vector of chunks is then hashed into a Merkle tree and the guest is given the root.

When the verifier wants to check the receipt, they first repeat the same Merkleization procedure as the prover, starting from the source image. If they started with the same image, they will get the same root. They can then compare this root with the commitment in the journal. If it is equal, the can be assured that the prover ran the guest with the same image as the verifier expected.

In the waldo_core::merkle module is implemented a wrapper on the merkle_light crate with support for using the SHA-256 guest circuit, and providing a VectorOracle abstraction. In the waldo_core::image module is implemented a specific MerkleTree type for images, and an ImageOracle type which can be used in the guest for image operations. These modules implement the ideas described above.

Similar Merkle tree abstractions can be used to, for example, ensure a secret word is part of a dictionary, a payment destination is not in a list of banned addresses, or that a user is in the set of authorized users.

Image Manipulation​

In order to manipulate the image and cut-out Waldo, and in particular to crop and apply a mask, this example utilizes the popular image crate. This is enabled by implementing image::GenericImageView on ImageOracle. With that trait, many of the image operations provided in the image crate, and by others, can be used on ImageOracle inside the guest. A similar approach could be used to produce a provable blur, image down-scaling, and more.

One the most powerful aspects of RISC Zero is the ability to use your favorite libraries, and avoid reinventing the wheel.

Get Involved​

Just as the current ecosystem of amazing open-source applications is powered on amazing open-source libraries, so will be the zkVM programs you write. And if you ever try to import a library and it doesn't work for some reason, it would be greatly appreciated if you let us know by filing an issue on GitHub.

Run this example​

You can find the source code and build instructions for this example (and many others) in the risc0/examples folder on GitHub. Run it yourself, and use it as a starting point to to create your own projects!

Note: This example is memory-intensive; we recommend using a machine with at least 64GB of RAM. If you run into issues, file a GitHub issue or ask for help on Discord.

· 8 min read
Tim Zerrell

At RISC Zero, we envision a future with boundless computation built on zero knowledge proofs. Today, we took a major step toward implementing this vision with tools available to all. We published v0.15 of the RISC Zero zkVM, which includes one of my favorite features: continuations.

In the context of our zkVM, continuations are a mechanism for splitting a large program into several smaller segments that can be computed and proven independently. This has many benefits, for instance:

  • Parallelizing proving
  • Enabling pausing and resuming a zkVM (similar to a “warm start” on AWS Lambda)
  • Limiting memory requirements to a fixed amount, regardless of program size

I discuss each of these a bit more at the end of this post, but the main benefit I'll focus on today is that with continuations, programs are no longer bounded by a fixed maximal length of computation. With continuations, programs can run for however many instructions it takes to get the job done.

But what does an unbounded cycle count enable in practice? The pithy answer is that the possibilities are endless — our zkVM is general purpose and can run anything that compiles to RISC-V (e.g. Rust, but also C++, Go, etc.), and now, just like the device you're reading this on, our zkVM will execute programs for however long they take to complete. This possibility, while endless, is comprised of innumerable specific examples. For instance, with continuations, you can run an EVM engine inside the RISC Zero zkVM, and prove the state changes caused by an Ethereum transaction. By "you," I mean you, personally, right now, on your laptop. Whenever you like, you can head on over to our EVM example, check out the source code, and run it for yourself! In the meantime, keep reading for a deeper explanation on what continuations enable, including how we use them to prove the results of Ethereum transactions.

Running the EVM on the RISC Zero zkVM​

Erik recently described how the RISC Zero zkVM differs from a zkEVM. That post is worth reading in full, but I'm going to gloss over the details and nuances and instead pull a single key quote:

On the zkVM, you can run just about any software that runs on a computer rather than anything that can run on Ethereum.

The EVM is software that runs on a computer. This quote, then, suggests that the EVM can be run inside our zkVM — and indeed it can. In fact, a few different teams have done this already: Odra wrote a proof of concept with SputnikVM, zkPoEX also uses SputnikVM to produce proofs of exploits, and we have an EVM example using revm.

The revm crate is a Rust-based EVM interpreter. Like most Rust crates, the revm crate can be run in the RISC Zero zkVM. Our example does exactly that. When you point it at an Ethereum transaction, our example will use revm to execute the transaction to compute the new state. It will then create a receipt containing the difference in state after the transaction has been executed and a zero-knowledge proof that this result is accurate.

Before continuations, this process worked only for small transactions. Therefore, when we published our EVM example, we used this small transaction as a demonstration so we could prove the transaction without hitting the cycle cap. However, since we hadn't yet added continuations to the zkVM, we also published our EVM example with a warning that it wouldn't work for all transactions, and in particular was unlikely to be able to prove transactions with elliptic curve precompiles.

With continuations, we no longer have this limitation. You can, for instance, prove this fairly heavy transaction for a contract using the ecrecover precompile and 5 KECCAK256. On my M1 Max MacBook Pro, this took about 12 minutes and about 12 GB of memory. The runtime will of course vary from system to system, and depends on the length of the program execution. The memory requirements, however, should be similar regardless of what system you run the proof on, and also regardless of the length of your program.

And to be clear, it’s not just that this particular transaction can now be proven on the zkVM. It’s all transactions: with continuations, any Ethereum transaction can be proven on the RISC Zero zkVM using our EVM demo, and there is no limit on transaction size.

What Is a Continuation?​

I mentioned at the start of this post that continuations are "a mechanism for splitting a large program into several smaller segments that can be computed and proven independently." This mechanism works by tracking the state of the zkVM at the start and end of each of these smaller segments, in the form of Merkle trees of the memory image (plus the program counter). This lets us compare the ending state of one segment to the starting state of the next.

A zkVM program is automatically split into segments, based on the cycle count. If the program would run for more cycles than allowed in a single segment, it is automatically split. We use the term "session" to mean sequence of segments where the first segment was initiated by the user and the final segment was terminated by the user (as opposed to being terminated by an automatically generated split). Thus, while segments have arbitrary boundaries determined automatically to stay within the per-segment cycle limit, sessions instead represent semantic boundaries, both starting and ending at the request of a user.

A session receipt consists of multiple segment receipts, and is validated by confirming that:

  1. each segment receipt is valid,
  2. the starting receipt of each segment matches the ending state of the prior segment, and
  3. the initial state (or image_id) matches what the validator expects (that is, that session is running the same code the validator wants to validate).

Benefits of Continuations​

As discussed with the EVM example, one of the most immediately apparent benefits of continuations is that you can now run a RISC Zero zkVM program for as long as you need to get the job done. But continuations enable more capabilities than just this. I want to touch on three I mentioned in the introduction: parallelization, pausing, and memory.

Parallelize​

These small segments can be distributed to many computers to parallelize the workload and reduce latency. The plan for where a zkVM program is split into segments and what work is done in each segment is computed ahead of proving by an "execution" phase. This gives a plan for proving each segment that is independent of the contents of all of the other segments. Thus, the hard work of proving the segments can be distributed amongst many systems, parallelizing the workload and reducing overall latency of the full proof.

Pause-Resume​

With continuations, a zkVM program can be paused and resumed. When describing segments, I mentioned that they lasted until the user asked for them to stop. This can be a traditional halt, indicating the end of computation. But it can also be a pause, which lets the user say "I want to do some computation now, and then come back at some later time and pick up where I left off."

For example, imagine a zkML workload in which an ML model is constructed, its weights are loaded, input data is provided, and an output is computed. In this example, the zkVM could be paused after the weights are loaded, just before input is provided. This has a couple of advantages. First, the model construction and weight loading could be performed prior to the user providing inputs, reducing the latency between inputs and outputs. Moreover, this initial setup phase could be performed once and paused, and then resumed multiple times for different inputs, saving the work of re-executing the shared setup.

Fixed Memory Requirements​

Prior to continuations, when a zkVM program took twice as many cycles, it roughly doubled the runtime and also roughly doubled the memory requirements. With continuations, memory requirements depend on segment length rather than total program length, so that programs of arbitrary execution length require a fixed amount of memory to run.

Continuations and Bonsai​

Continuations are a powerful tool. We want to simplify the complexities of continuations, and zero-knowledge proofs more generally, as much as possible. To this end, we are working on Bonsai, and so here I want to mention a few of the complications we expect Bonsai to simplify.

For one, while there is the potential for substantial latency improvement through parallelization, orchestrating the distribution of a program's segments is not built into the zkVM code.

For another, we currently only support flat continuations and not rollup continuations. With flat continuations, each segment produces its own receipt. Each of these receipts needs to be individually verified, and while we have helper functions to prove the overall program, the required verification work still increases with execution length. Rollup continuations would use proofs of verification to recursively rollup these individual segment proofs. The result would be that only a single receipt would be necessary for verification, and verification time would be constant regardless of execution length.

We are working on Bonsai, which we believe addresses these challenges and more. We expect Bonsai to make the power of zero-knowledge proofs and continuations easily accessible. If you're interested, sign up for the Bonsai waitlist!

· 6 min read

We recently participated in ZKHack Lisbon, ZK Hack's first in-person hackathon. Thanks to everyone who contributed projects!

Below is a list of all RISC Zero prize winners from ZK Hack Lisbon. We've provided longer descriptions for these projects as an added thank you to the four teams that won $2000.

To support future hackathon participants, we've included why our judging team loved the top projects. Our judging criteria will vary from hackathon to hackathon, but we're excited to see development in emerging ZK application spaces, inventive uses of ZK tech, and projects that demonstrate the simplicity and power of ZK. And because doing is teaching, we love submissions that either contain self-explanatory educational content or insightful supplementary docs.

RISC Zero Prize Categories​

We encouraged participants at ZKHack Lisbon to submit two types of project entries:

Problem description
Challenge #1Build an application that uses the RISC Zero zkVM.
Challenge #2Write code that utilizes data serialization or deserialization crates in the guest.

RISC Zero Hackathon Prize Winners

Winning Team Projects: $2000 Level​

Mindf*ck: Code Obfuscation For Fun And Profit​

To obfuscate code execution, the Zeroskill team has added a Rust-based Brainf*ck interpreter to the guest program. With this addition, the execution of an interpreted program is captured by the guest zkVM.

As an example, the following "Hello, World!" program string might be passed into the guest as program input:

--<-<<+[+[<+>--->->->-<<<]>]<<--.<++++++.<<-..<<.<+.>>.>>.<<<.+++.>>.>>-.<<<+.

The guest's public outputs consist of the executed "Hello, World!" program's final memory state, the values which the Brainf*ck program dictates should be written to stdout, and a hash of the program source (the string shown above).

Even setting aside code obfuscation, this is a fantastic example of how easily nontrivial Rust code may be written for the zkVM. From an educational perspective, we loved that this team created an example of interpretable code as input (and memory layout as output!).

Zero-Knowledge Decision Tree Prediction​

This team tackled a popular use case for ZK in machine learning: how can an ML provider make trustworthy predictions without disclosing their model? This problem arises in applications when the ML model is sensitive enough that releasing it might become a privacy issue.

Categorical classification with decision trees starts with a tree built from labeled data. Starting at the tree root, feature values are used to guide decisions about which path to follow down to a leaf node representing a single category as the outcome.

As a demonstration, this team's guest zkVM program used a hard-coded decision tree based on the IRIS dataset, which categorizes flowers based on their measurements. Measurements for a single flower are passed into the guest, and the classification result is added to the journal as public output.

Building an ML solution is an ambitious hackathon project. We thought that the team made great decisions about algorithms and implementation details to effectively demonstrate ZK's potential for ML in a weekend. The accompanying demonstration elevated this project from an interesting ML submission into a nice educational piece.

Zero-Knowledge Wordle​

This project implemented a fair version of Wordle, in which a client makes word guesses against a server that generates feedback in the form of receipts. The journal of each receipt contains feedback about the client's word guess (i.e., "right letter, wrong position") as well as a hash of the correct answer.

The server is considered 'fair' because the client can detect whether the server moves the target during play. To accomplish this, the client confirms that the hashed correct answer has not changed from receipt to receipt.

Although the idea of playing fair Wordle isn't new, the architecture for this project was easily as interesting as the game design. The RISC Zero server uses a RISC Zero prover behind an API server. The gameplay results are stored in a contract on chain. As a working example that demonstrates running a RISC Zero verifier in WASM, we particularly appreciated the browser-based client.

Proof of Physical Item Using NFC Devices With On-Device AES Keys​

This project used ZK proofs to implement message signature verification. This team used NTAG 424 chips that include an on-device AES key and support for AES-128 encryption operations.

When the NFC device is tapped, NTAG creates a SUN (Secure Unique NFC) message using an AES key, a read count, and a UID. In this project, the signed NFC message is checked by regenerating the SUN message in a guest program and confirming the messages match.

The AES key and UID remain constant for each device and are hardcoded into the guest program. (Note that this means each receipt must be verified with an image ID unique to the device on which it was generated.) The read count and expected SUN message are passed as guest inputs. Within the guest, the read count, hardcoded key, and hardcoded UID are used to generate a fresh SUN message for comparison.

We loved that this project interacts with a hardware solution and presents an interesting proof of concept for proximity-based physical interactions. We especially appreciated the use of AES in the guest.

Winning Team Projects: $1000 Level​

RISC Zero HMAC Implementation​

Dread Pirate Roberts Marketplace: A zkReputation-Based Marketplace For High-Value Transactions​

Winning Team Projects: $500 Level​

Ting Tong: A Turn-Based Guessing Game​

Whitebox: Composable, Transparent, Configurable, and Verifiable Algorithms​

Crosschain Escrow on L3 \<> L1 Validity Rollups​

Keep on hacking <3​

If you missed this zero-knowledge hackathon, you can connect with participants and find out about new events at the ZKHack Discord. If you're curious about the other ZKHack Lisbon winners, take a peek at this Twitter megathread. And while you're at it, stop by the RISC Zero Discord and say hello!

· 7 min read
Erik Kaneda

As the current smart contract landscape increases in complexity, with dapps becoming more advanced and blockspace more scarce, the costs of running on-chain code are only increasing. In other words, if your DeFi logic is becoming computationally expensive or your on-chain game logic needs the extra compute power, you should be looking at using a zkVM or zkEVM to move the complex application logic off-chain.

In this blog post, I want to explain the difference a single letter can make in this context. I’ll start with an overview of EVM, followed by zkEVM, and move on to zkVM. While zkEVMs allow you to transport Solidity applications off-chain, RISC Zero’s zkVM and the upcoming Bonsai network allow you to write scalable, chain-agnostic code using Rust.

Quick overview of EVM:​

EVM stands for Ethereum Virtual Machine, and you can think of it as software that performs all the transactions on Ethereum. Each node participates in the Ethereum network by running this software (implementations such as geth). In Ethereum, the transactions are represented by code in a format called the EVM bytecode which represents instructions for the EVM. Largely, these instructions are geared toward mathematical computations, getting information about the blockchain, and exchanging money. There are many virtual machines out there in the world and each one has its own specialty. Ethereum’s virtual machine is critical because it is more specialized towards decentralized finance (DeFi).

What is “zk” and why is everyone placing it in front of other words?​

One of the coolest trends these days is to put “zk” at the front of words where these letters stand for zero-knowledge proofs. There are many examples on wikipedia (my favorite being the “Two balls and the color-blind friend” problem). If you’re unfamiliar with them, I suggest taking a few minutes at this point to read an example of a zero-knowledge proof.

Long story short, zero-knowledge proofs enable verifiable computing. You can think of this as a way to ensure which computation was done and that the result of the computation is correct. One way for computers to agree on a result of a computation is for each machine to run the same code and compare the results. Depending on the computation, this can be expensive for systems with limited resources. By using zero-knowledge proof frameworks like RISC Zero’s, machines can ensure that the computation executed correctly by checking the mathematical validity of the proof instead of running the same code.

Here at RISC Zero, we refer to these proofs as “receipts,” and I’ll use this terminology for the rest of the blog. Each receipt includes a cryptographic identifier that indicates which computation was done as well as a log of any public outputs of the computation. While this may seem like a simple concept, it means that machines can generate receipts to “prove” that a computation was done.

So what happens when you put zk in front of EVM?​

The term zkEVM is used to describe software that runs a smart contract on the EVM bytecode engine and generates a receipt for a particular computation (or transaction). This software can usually prove that two or more receipts are valid and generate another receipt. By using this mechanism, zkEVMs can run many transactions and represent it using a single receipt and this is referred to as a “rollup”. Rather than doing all computations on-chain, projects written in Solidity can use zkEVMs to scale transactions by posting a single receipt on the blockchain to represent many transactions that happen off-chain. There are many types of zkEVM’s and if you want to learn about them, you can read more in this article.

zkVM: Freeing Verifiable Computation by dropping the E​

At RISC Zero, we implement a zero-knowledge virtual machine (zkVM) rather than a zkEVM. The difference between the two is that a “VM”, which stands for “virtual machine”, is more general than the EVM. On the zkVM, you can run just about any software that runs on a computer rather than anything that can run on Ethereum. This computer uses the RISC-V architecture which is a set of instructions used for general-purpose computing. This means that RISC-V doesn’t have a notion of wallet addresses or other blockchain constructs built in. The instruction set is mostly composed of operators that move data between memory locations and do mathematical operations on data. While this instruction set may seem overly general, there is no requirement for programmers to know how to program in assembly language in order to write programs for this zkVM.

In contrast to the EVM, this underlying RISC-V emulator allows programmers to write in languages such as Rust, C/C++, and Go for the zkVM (note, we currently support Rust and our C/C++ and Go support is currently in-progress). This means that programmers for the zkVM can use relevant libraries that others have developed within the language’s ecosystem. One example is that we can run programs that play games like Wordle or Where’s Waldo. However, we aren’t limited to simple games: you can run many other programs that compile to RISC-V.

What’s so useful about running RISC-V programs?​

If you started reading about this because you wanted to learn more about frameworks that can help you write better DeFi apps, you might be wondering why we are working on such a generic computation framework. By allowing users to write programs using general-purpose languages, we open up the possibilities to writing code outside of Solidity libraries. This means that the application logic does not need to be limited to what can be expressed using Solidity and allow you to write chain-agnostic code. General-purpose languages like Rust allows developers to write different kinds of programs more easily than languages that are designed for a specific purpose. For example, you can write a simple arithmetic calculator using Rust that takes a mathematical expression as input, runs the mathematical computation, and returns the solution as the output. If you increase the complexity of this calculator to support common programming language constructs such as variables, loops, and functions, you’ve implemented a simple language interpreter that take a program as the input, runs the program, and returns the solution as the output. These programs can be compiled to RISC-V and run on RISC Zero's zkVM. With Rust, you could use existing crates to program your application instead of writing everything from scratch.

One such library is the revm crate on rust. This crate is an implementation of EVM that is written in Rust. By using this crate, we can run an EVM bytecode interpreter on the zkVM. This means that you can run solidity contracts on the EVM bytecode interpreter that runs on the zkVM! By doing so, the zkVM generates a receipt that represents execution of the EVM running a smart contract. This has been explored in this blog post by Odra and has been used by the zkPoEx team to improve bug bounties.

How to scale blockchains​

As the current smart contract landscape increases in complexity, many people find that the on-chain code they maintain will only increase in cost as they develop it. In other words, if your DeFi logic is getting to become computationally expensive or your on-chain game logic needs the extra compute power, RISC Zero’s zkVM and the upcoming Bonsai network allow you to write scalable chain-agnostic code using general purpose programming languages! I’ve listed a few examples in this blog post, and we are at the very beginning of truly scalable computation network. If you want to see what this is all about, get started today, join our community, sign up for bonsai and help build a decentralized and scalable internet for all.

· 3 min read
Paul Gafni

First off: huge thanks to all the organizers and participants at ZK Hack & ZK Summit! Both events were fantastic; I'm already looking forward to next time.

Now that the jetlag is behind me, I wanted to share some zero-knowledge research threads that I'm excited to keep thinking about and talking about.

Folding Schemes: Nova, Supernova, and Sangria​

Video Reference
Blog Reference

This is perhaps the most important emerging idea in zk research right now. These schemes achieve Incrementally Verifiable Computation (IVC) by combining instances that haven't been proven. This contrasts with the more familiar approach of proving each instance and then rolling up the results.

Nova introduced a technique for combining R1CS instances. Supernova generalized Nova to support arbitrary instruction sets. Sangria uses the same technique in order to combine (relaxed) PLONK instances.

A natural research question arises: can we apply this approach to AIR-FRI STARKs? The answer isn't obvious, as this technique depends on a homomorphic encryption scheme such as KZG.

The Red Wedding​

Video Reference

This idea, proposed by the team behind TritonVM, aims to reduce the verification time (and thus, the recursion time) in a STARK system by shifting work from the Verifier to the Prover. Specifically, the Prover can generate a SNARK proof in order to alleviate the need for the Verifier to evaluate the AIR constraints at the DEEP query point.

Some research questions:

  • How does the computational cost of the inner SNARK verification compare to the cost of the AIR evaluation that it aims to replace?
  • What commitment scheme should be used for this inner SNARK?
  • What's the right scope for the SNARK verification? Should it include arithmetic or hashing operations in addition to the AIR constraint evaluation?

LogUp: Batched Lookup Arguments​

Video Reference
ePrint Reference

In contexts where the Prover is repeatedly doing the same lookup, LogUp reduces the number of columns necessary in lookup tables by ~50%, relative to PLOOKUP. About 30% of the witness-generation in RISC Zero is spent generating columns for a PLOOKUP-based lookup argument; we're looking into switching to LogUp for future versions.

The premise here is that by making use of logarithmic derivatives, we can transform a grand product accumulation into a (cheaper) grand sum accumulation. The LogUp paper (linked above) frames this technique in terms of a multivariate IOP; the Tip5 paper describes a version of this technique that's better suited to the univariate context.

The Mersenne Prime 231−12^{31}-1​

Video Reference
Slides

In Denver last month, Daniel Lubarov discussed the idea of using the finite field of order 231−12^{31} - 1 for building Plonky3. This field is particularly nice for handling finite field arithmetic, since 231=12^{31} = 1. The major obstacle is that the multiplicative group of this field isn't good for NTTs, since 231−22^{31} - 2 doesn't have many 2s in its prime factorization.

There are a number of options for how to make this work:

  • changing from a FRI-based commitment scheme to one based on Orion or Brakedown
  • using a mixed-radix version of FRI that doesn't depend on high 2-adicity
  • doing NTTs in a quadratic extension field (note that the multiplicative group of the quadratic extension has order 262−2322^{62} - 2^{32} and therefore has 2-adicity of 2322^{32})

Looking forward to seeing what the Polygon Zero team is brewing up on this front.

Don't be a Stranger!​

We'd love to hear what you're thinking about, in regards to these questions or otherwise. Continue the conversation on Discord at ZKHack or RISC Zero.

· 5 min read
Paul Gafni

We are thrilled to share the recent success of a groundbreaking project, zkPoEX (Zero-Knowledge Proof of Exploit), which won 1st place in the ETHDenver Hackathon DeFi Track. zkPoEX enables secure collaboration between security experts and DeFi projects.

Built using RISC Zero’s zero-knowledge virtual machine (zkVM), zkPoEX is a Proof of Concept (PoC) that showcases a simple reentrancy case; it's an exciting application of zero-knowledge technology in the DeFi landscape.

The Challenge in DeFi Security

Bug bounty programs in the DeFi space can be challenging to manage and maintain. They aren't always honored, and compensation for white hat hackers may not be sufficient. This lack of incentive can lead to unreported vulnerabilities, ultimately resulting in a less secure DeFi ecosystem.

Enter zkPoEX: A Game-Changing Solution

zkPoEX addresses these concerns by enabling white hat hackers to report live vulnerabilities in smart contracts while maintaining the confidentiality of the exploit. This could allow auditors to safely generate a zero-knowledge proof of exploit without revealing the actual exploit. With zero-knowledge proofs, the auditor can prove that they know of a transaction that can produce an undesirable change of state in certain contracts, without revealing the specifics of the exploit.

Consequently, projects are incentivized to collaborate with auditors to fix the vulnerability, fostering a stronger relationship between hackers and project owners. The result is a more secure DeFi ecosystem where vulnerabilities are addressed effectively and confidentially.

Proof of Concept: Simple Reentrancy Attack Case

To demonstrate a reentrancy attack, a basic Ethereum Virtual Machine (EVM) implementation requires the following components:

  • A Target Contract
  • An Exploiter Contract
  • A Caller address (Externally Owned Account)

To execute the attack, the Caller address sends a transaction with calldata to the Exploiter Contract, which in turn interacts with the Target Contract and repeatedly calls back to the Exploiter Contract to reduce its balance. This exploits a flaw in the Target Contract's code that allows reentrancy.

Inside the RISC Zero zkVM​

To execute the attack within the RISC Zero zkVM environment, a Rust-based EVM implementation is required. For this proof of concept, zkPoEX has selected SputnikVM as the implementation of choice.

Architecture​

The Host requires private inputs like the calldata being sent by the Caller and the bytecode of the Exploiter Contract, as well as public inputs like the global state of the blockchain, which includes information such as the gas price, chain ID, and the state of every account that's involved in the transaction, including nonce, balance, storage, and code.

The interaction within the EVM is defined by the Guest, which involves a single transaction from the Caller to the Exploiter Contract. Constraints are enforced in the Guest: success of the transaction and the use of different addresses for the Caller, Target, and Exploiter Contracts. The Host shares private inputs with the Guest, which it then uses to execute the transaction. The Prover, acting as a white hat hacker, provides both the public and private inputs and performs the method execution.

Outcomes​

After the execution the receipt is generated, which can be used to verify the validity of the computation and results. The journal contains committed information such as the hash of the public state, change state such Target Contract balance decrease, and a commitment of the private input, that is, a hash of those private inputs.

Once the execution is completed, a receipt is generated, which can be used to verify the validity of the computation and results. The journal includes committed information, which consists of the hash of the public state, changes made to the state, such as a decrease in the balance of the Target Contract, and a commitment to the private inputs, represented by their hash.

As a result of the versatile design of the zkVM it should be noted that: State change outputs may be customized or enforced according to specific requirements. For a more general approach, the Target Contract can be treated as a public input. The constraint system within the Guest can be made more complex, depending on the specific use case.

Running the PoC required zkPoEX’s team to reduce the number of interactions between the Exploiter and Target Contracts to reduce the amount of computation. That led to approximately 16GB RAM requirement and 4 minutes runtime using an Apple M1 Max with 10-core CPU and 32-core GPU.

zkPoEX and RISC Zero

Thank you to the zkPoEX team to collaborating with us to ensure this post was accurate.

zkPoEX was developed by @zkoranges and @feder.eth with acknowledgements to Daniel Lumi for advisory and Maciej Zieliński for his insightful blog post on EVM inside the RISC Zero zkVM.

zkPoEX's success in the ETHDenver hackathon DeFi track demonstrates the potential for zero-knowledge proof technology in securing the DeFi ecosystem.

The RISC Zero zkVM, with its ability to facilitate the creation and verification of zero-knowledge proofs, is uniquely positioned to power innovative applications like zkPoEX.

We, at RISC Zero, are committed to driving innovation in the field of zero-knowledge proof technology and expanding its use cases across industries. We look forward to contributing to the future of DeFi security and continuing our collaboration with projects like zkPoEX to ensure a safer and more robust financial ecosystem for everyone.

Stay tuned for more updates on the RISC Zero zkVM and its groundbreaking applications, and don't hesitate to reach out if you have any questions or would like to explore collaboration opportunities.

To find more info about zkPoEX:

· 10 min read
Steven Li

The RISC Zero team is out in full force for ETHDenver! Come to our talks, booth, and developer meetup to learn more about what we have been hard at work building.

Bonsai

The RISC Zero team is excited to announce: Bonsai our Zero-Knowledge Proving Network

Bonsai is a general-purpose zero-knowledge proving network that allows for any chain, any protocol, and any application to take advantage of ZK proofs for scaling, privacy, and more. With Bonsai, ZK proof integration into ETH, L1 Blockchains, Cosmos App Chains, L2 Rollups, DApps etc. is possible in a matter of days with minimal development effort. Bonsai is a new kind of blockchain: a massively parallel, chain-agnostic, and general-purpose network designed to allow application developers to build new classes of applications.

Our RISC-V zkVM acts as the foundations of Bonsai and enables wide spread language compatibility with the potential for zero-knowledge provable code written in Rust, C++, Solidity, Go, and more. With a combination of recursive proofs, a bespoke circuit compiler, state continuations, and continuous improvements to the proving algorithm, Bonsai enables anyone to generate highly performant ZK proofs for a variety of applications.

Bonsai combines three key ingredients to produce a unique network that will enable new classes of applications to be developed across blockchain and traditional application domains:

  • A general-purpose zkVM capable of running any VM in a ZK/verifiable context
  • A proving system that directly integrates into any smart contract or chain
  • A universal rollup that distributes any computations proven on Bonsai to every chain

Bonsai effectively allows for any application, blockchain, and appchain to easily integrate ZK proofs into their protocol without any custom ZK circuit development. This will enable a paradigm shift in how ZK proofs are used across the entire blockchain ecosystem.

The Bonsai Litepaper can be found AT THIS LINK.

🚀Get notified when Bonsai is released to the public🚀

The ETHDenver Bonsai Developer Website can be found AT THIS LINK.

💡 Early alpha access to Bonsai is currently controlled via a Whitelist.
💡 Developers looking to join the Bonsai Whitelist may fill out the form HERE

zkVM

One Page Overview

The RISC Zero zkVM is an open-source, zero-knowledge virtual machine that lets you build trustless, verifiable software in your favorite languages. The zkVM bridges the gap between zero-knowledge proof (ZKP) research and widely-supported programming languages such as C++ and Rust. ZKP technology enables programs' outputs to be checked for correctness by someone who cannot see its inputs. This verifiability enables game changing scalability and privacy across a wide variety of applications. The general-purpose nature of our zkVM also allows for it to be compatible across a variety of blockchain protocols.

The RISC Zero proof system implements a zk-STARK instantiated using the FRI protocol, DEEP-ALI, and an HMAC-SHA-256 based PRF. It also is compatible with recursion and has near unlimited proof complexity.

Current performance benchmarks can be found AT THIS LINK.

The RISC Zero zkVM Proof System Whitepaper can be found AT THIS LINK.

Getting Started​

The best place to started with our zkVM is our Docs. Within it you will find our project template, which acts as the foundations for any RISC Zero project. It will also help in giving a good feel for how each component of our project works together.

Moving on from this template, the RISC Zero Digital Signature Demo and Password Validity Checker are great examples of how our zkVM can be used to add security and privacy into existing technologies. Finally, our website and youtube channel have a variety of materials that should help you better understand the technical foundations of the RISC Zero zkVM.

ZKHack zkVM Demos

Our ZKHack presentation included a number of examples of zkVM projects. The full presentation can be found here. All demos can be found here.

Where to Find Us

Come to Our Talks!​

Building a Central Limit Order Book on Ethereum using ZK​

Brian Retford
Feb 27, 2023 11:10 AM - 11:30 AM MST
#BUIDLHub Mainstage, #BUIDLHub | 3403 Brighton Blvd, Denver, CO 80216

Zero-Knowledge Proofs have a lot of promise for both increasing privacy and scaling by verifying the correctness of off-chain computation. However, the development of traditional circuit based ZKPs is challenging, since the programmer needs to learn new languages, new concepts, and new development tooling. A new class of Zero-Knowledge Virtual Machines is attempting to allow ordinary code, such as Solidity or Rust to run inside ZKPs. This talk will describe how such ZKVMs work, including a basic background on ZKPs, arithmetic circuits, permutation arguments, and representations of memory, as well as providing resources for getting started using ZKVMs to implement off chain logic.

Just Prove It: ZK & the Future of Scaling​

Ash Schap
Mar 03, 2023 11:05 AM - 11:20 AM MST
Main Stage, National Western $SPORK Castle | 4655 Humboldt St Denver CO 80202

Zero-Knowledge Proofs will change computation as we know it, both inside Web3 and outside of it. But what do we need to get started on this vision? This talk will outline a generalizable, protocol-focused approach to empowering developers with accessible ZK tooling, unlocking the power of ZKPs for dapp and app developers and leading to the advent of truly scalable, verifiably correct computation for blockchain applications.

Zero-Knowledge Virtual Machines: Running Rust code inside a Zero-Knowledge Proof​

Jeremy Bruestle
Mar 04, 2023 1:30 PM - 1:50 PM MST
Decentralized Finance Stage, National Western $SPORK Castle | 4655 Humboldt St Denver CO 80202

A deep dive into how ZK can be used to execute complicated logic like order book matching off chain to build powerful apps on chain

If Knowledge is Power, What is Zero-Knowledge? An Intro to zkVMs​

Erik Kaneda
Mar 04, 2023 2:00 PM- 2:20 PM MST
Bunny Slopes, National Western $SPORK Castle | 4655 Humboldt St Denver CO 80202

In the past decade, we have seen the rise in popularity of zero-knowledge proof systems along with terminologies that are used to describe them such as STARK, SNARK, PLONK, etc. But what sorts of applications does zk tech actually enable? This talk aims to illuminate what is possible today through zkVM’s and what it means to write programs for them. The focus of this presentation is to describe the features of a zkVM and how developers can use it to build applications on blockchains and beyond!

Delendum Future Computing Research Workshop​

  • Brian Retford, Our ZK-Enabled Future
    • Mar 01, 2023 10:45 AM - 11:00 AM MST
  • Tim Carstens, Practical Benchmarks for ZK Systems
    • Mar 01, 2023 2:00 PM - 2:15 PM MST

RISC Zero Developer Meetup​

Click Here To Register Now!
Feb 27, 2023 4:00 PM - 6:30 PM MST
Shift Bannock | 1001 Bannock St, Denver, CO 80204

  • 4:00 - Sign-In + Social
  • 4:20 - ZK Panel + Questions
  • 5:00 - Break
  • 5:15 - Group Discussions
    • General ZK Developer & Ecosystem Concerns
    • zkVM & AppDev
    • Platform & Integrations
  • 6:00 - Signups + Social + Feedback

Booth Location​

Come stop by our booth to meet the team and try live demos of our zkVM in action!

The booth is at marker (X) located inside the DeFi District next to the Coffee Lounge (15)

RISC Zero Booth Location

Bounties

ETHDenver Bounty Page: https://app.buidlbox.io/guidl/risc-zero

Bounty #1: Build on RISC Zero or Integrate RISC Zero into your project​

RISC Zero’s core technology is our RISC-V Zero-Knowledge Virtual Machine. On top of that, we’re building a zero-knowledge computing platform called Bonsai. Bonsai supports the ability to do arbitrarily complex computations in plain Rust and access proofs of those computations on-chain, effectively adding Rust support and zero-knowledge scaling to Layer 1 Ethereum.

Bonsai is currently in a pre-release stage and, as part of this bounty, we’d like you to build an application using Bonsai. Doing so requires getting early access, which you can request here. However, even prior to getting access, you can participate in this bounty.

To build such an application, you’ll need two major components: your application logic written in the form of zkVM guest code and a solidity contract as an interface to the Ethereum world. Communication between those two components will happen via the Ethereum Bonsai bridge.

Because Bonsai is in a pre-release state, we expect you to need some help getting going - to support this, we’ll have Bonsai developers available to help via discord (and a few in person, as well).

For application ideas, think about computationally intensive tasks. What have you always wanted to see on Ethereum but development complexity or gas costs/caps have kept you from building?

Prize Amount - 15,000 USDC

We are offering a total of 5 prizes, with a top prize of 7,000 USDC and a minimum prize of 2,000 USDC to qualifying projects.

We reserve the right to withhold prizing in cases where low-quality submissions do not meet our bounty requirements.

Resources​

💡 Early alpha access to Bonsai is currently controlled via a Whitelist.
Developers looking to join the Bonsai Whitelist may fill out the form HERE

Bounty #2: Reduce the RISC Zero zkVM boilerplate by removing the methods crate​

Allow RISC Zero zkVM code to be written without needing to invoke specialized build code for the guest. In particular, after fulfilling this bounty zkVM users will be able to:

  • build guest code in the same crate and workspace as host code
  • build guest code without using a custom build.rs script
  • freely locate the guest code in whatever part of the source tree is most sensible for their project
  • without reducing the functionality or performance of the zkVM.

This means a successful completion of the bounty will be able to take zkVM guest code, compile it into an ELF binary, and supply that binary to for the host to use all while meeting the above requirements.

We believe that this bounty would be most easily accomplished by using the bindeps artifacts dependency functionality of Cargo, described here. Use of bindeps is not a requirement of the bounty, but we do believe it is the most likely path to successfully accomplishing the bounty.

Prize Amount - 5,000 USDC

In the case of multiple bounty submissions meeting our criteria, we will split the prize among successful submissions in proportion to their completeness and code quality, as described above. At our discretion, we may award a partial prize to submissions that make substantial but incomplete progress towards fulfilling the four criteria outlined.

We reserve the right to withhold prizing in cases where low-quality submissions do not meet our bounty requirements.

Resources​

Bounty Support​

Connect directly with our team for any help regarding the bounty and hackathon on our Discord!

https://discord.gg/risczero

Contact Us

Reach out to us this ETHDenver through our Discord LINKED HERE

Get notified when Bonsai is released to the public!

Interested in partnering with us? Let us know HERE

· 4 min read
Manasi Vora

Excited to announce that I have joined RISC Zero as the VP of product growth. We are building a general-purpose zkVM and ushering the wave of ZK compute for all!

If you know me, you know I have done my research! As I explored my next career move, I scanned the entire crypto landscape and had conversations with numerous companies. I am most excited about DeFi's potential to solve real financial challenges, DAOs as revolutionary coordination mechanisms, and decentralized infrastructure (storage, compute, identity, etc.) as essential building blocks for disintermediation.

The 2020-22 period brought significant growth in the crypto industry, attracting widespread attention and new talent. The rising popularity of DAOs, the explosion of DeFI applications, and the NFT boom were all made possible by the previous cycles of infrastructure building. But very quickly, we hit scaling barriers, exposing the gaps in our infrastructure.

Bear markets give us the space to build infra needed for the next wave of adoption. We are again in the infrastructure part of the app-infra cycle for crypto.

Refer this USV piece on the myth of infrastructure.

And today’s infrastructure will bring tomorrow’s killer app.

One thing I knew for sure: I wanted to work on something that truly moves the needle for crypto use cases and adoption. Having worked on decentralized storage infra for the last 3.5 years, I have witnessed first-hand the difficulties developers encounter when building complex real-world applications on-chain.

ZK tech is uniquely positioned to address the challenges facing crypto infrastructure today by enabling verifiable complex computations off-chain. Here’s an explanation from ChatGPT’s 😎

In the past six months, there have been remarkable advancements, resulting in a surge of teams developing ZK scaling solutions. ZK protocols and applications enabled by ZKPs are still in their infancy, and the excitement is only going to be multifold this year. If we can harness the potential of ZK and make it available to developers of all levels, we can open up a whole new realm of previously impossible applications. Jill Gunter predicted ZKP applications becoming the norm. I think we will be seeing it sooner than 2026!

Building ZK circuits, leveraging ZKPs, and building ZK applications is no small feat! Requires millions of dollars of investments, assembling a team of rare crypto and math experts, and learning new custom programming languages with inadequate tooling.

Enter RISC Zero!

RISC Zero is removing these resource and time-intensive barriers by bringing existing languages, tools, and developer skills to ZKP development. Built on the open RISC-V instruction set, RISC Zero’s zkVM will enable developers to generate highly performant ZKPs for a variety of applications with code written in Rust, C++, Solidity, Go, and more.

When choosing my next project, my top priority was the people involved and the potential impact it would make. One of the best things about joining RISC Zero is its team of brilliant individuals with decades of experience across distributed systems, cryptography, security, and cloud computing. The combination of technical expertise and genuine kindness is truly rare!

RISC Zero will play a key role in ushering in the era of verifiable computing. We are bringing trusted computing into trustless environments. And I couldn’t be more excited to work on this alongside Brian Retford, Jeremy Bruestle, Choong Ng, Frank Laub, Ash Schap, and the rest of the team.

If you haven’t guessed already, I am totally ZK pilled. And you will be too! I will be posting accessible ZK content, so join me in this journey @manasilvora.

HMU if you want to chat ZK or are building an L2 rollup, appchain, dapp, or an L1 that wants to leverage ZK tech!

Alright, back to building!

· 10 min read
Bolton Bailey

Hello everyone! I'm Bolton Bailey, a Ph.D. student and software engineer at RISC Zero. I'm writing this blog post to discuss a project that I've been working on, in conjunction with Runtime Verification Inc., to run a Metamath checker inside the RISC Zero zkVM. Although this project is just getting started, I think it's headed in a very exciting direction. In this post, I'd like to share with you all what makes it so interesting, how we've gone about it, and what it could look like going forward.

What are Formal Methods?​

My field of research lies at the intersection of cryptography and formal methods. Formal methods are a mathematically rigorous approach to software development that ensures a piece of code does what it is supposed to do. A formal methods approach goes farther than simply examining a piece of code line-by-line or writing a test suite to ensure the code runs correctly on a number of examples. Instead, we write out a mathematically precise specification of what the code is supposed to do and prove that the code will always behave as specified, no matter what input it is given.

Rather than writing down specifications and proofs on paper and checking them by hand, we get the computer itself to help us. Formalists use specialized computer languages known as formal systems to express their proofs, and they write programs to check these proofs so that they can be sure they made no mistakes. The language I've been working with is the Metamath system.

What is Metamath?​

Metamath is a formal system that's designed to be flexible enough to represent proofs in a variety of mathematical frameworks, but also very simple for the computer to understand. The way a computer processes logic can be unintuitive for a human, but this section will hopefully give you an idea of how it works.

Here is an example of some simple Metamath code from the manual. This code describes a simple mathematical system for talking about numbers, with addition and zero as the basic concepts:

$( Declare the constant symbols we will use $)
$c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
$v t r s P Q $.
$( Specify properties of the metavariables $)
tt $f term t $.
tr $f term r $.
ts $f term s $.
wp $f wff P $.
wq $f wff Q $.
$( Define "term" and "wff" $)
tze $a term 0 $.
tpl $a term ( t + r ) $.
weq $a wff t = r $.
wim $a wff ( P -> Q ) $.
$( State the axioms $)
a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
a2 $a |- ( t + 0 ) = t $.
$( Define the modus ponens inference rule $)
${
  min $e |- P $.
  maj $e |- ( P -> Q ) $.
  mp $a |- Q $.
$}
$( Prove a theorem $)
th1 $p |- t = t $=
$( Here is its proof: $)
tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
tt weq tt tze tpl tt weq tt tt weq wim tt a2
tt tze tpl tt tt a1 mp mp
$.

There is a lot of boilerplate, but the critical part of the definition is the two axioms listed on the lines that start with a1 and a2. Respectively, these axioms state that:

  1. If t = r and t = s, then r = s.
  2. For any term t, t + 0 = t.

As an example of how detailed these proofs can get, let's unpack the very last theorem at the end of the example above, which proves t = t for any term t. The proof consists of a very low-level list of invocations of rules and axioms that show the theorem holds. At a high level, the proof says that if we substitute t from the first axiom above with t + 0, and r and s are substituted for t, then the first axiom becomes "If t + 0 = t and t + 0 = t, then t = t". By the second axiom listed above, the t + 0 = t conditions hold; therefore, the first axiom is telling us that t = t. Notice that we have to use the first axiom once and the second axiom twice (once for each condition of the first axiom). While not all of the symbols in the proof of th1 might be familiar, we can see it includes one reference to a1 and two references to a2.

This may seem like an overly convoluted way of proving a very simple fact. This is because computers need to have every detail spelled out to them. Metamath in particular is designed to not have a lot of built-in optimizations, in order to keep the Metamath checking program as simple as possible. Unlike a human, the Metamath needs to be reminded of the fact that "t is a number" every time t comes up again in the argument. This is essentially what the tt token does - you can see it comes up 15 times in the proof of th1!

What are the possibilities for formal methods?​

The example theorem above is a simple one. In principle, however, there's no limit on what can be proven within a formal system like Metamath: we can describe logical systems that deal with set theory or even outline the semantics of programming languages. Within formal methods, programs and data are just different types of mathematical objects, ones for which confidence can be of the utmost importance. The software industry in general, and the cryptocurrency industry in particular, has a lot at stake when it comes to bugs in their systems: billions of dollars have been hacked out of blockchains, and entire organizations exist that look to use formal analysis to help plug these holes.

Zero-Knowledge Proofs for Formal Methods​

Having established what formal methods are and why they're useful, let's ask why someone might want to use succinct zero-knowledge proofs in conjunction with them.

Suppose a technology firm wants to be assured that their products have no bugs. They open a bug bounty and offer a prize to anyone who can find a flaw. A formal analysis firm writes a specification of what the code is supposed to do and then attempts to find a proof that the code meets the specification. In their analysis, they end up finding a bug, and they create a formal proof that the specification is not satisfied.

At this point, the formalist firm is nervous that the software writers will look at the proof and say that actually, the bug isn't a problem at all, and this doesn't merit paying out the bug bounty. Besides, the technology firm doesn't want to run this long formal check themselves. It might not even be a technology firm offering the bounty at all, but instead a smart contract.The smart contract is limited in how much gas it can use, so it can't reasonably check the whole formal analysis.

This scenario is ripe for a succinct proof application. The formalists can prove the bug is real without a big data transfer or computation by sending a STARK proof that the formal proof check validated their code in Metamath or another formal system. As a bonus, they can make the STARK a zk-STARK if they are worried about someone seeing the proof, reverse-engineering the bug, and making an exploit.

Making it a Reality with RISC Zero​

How does all this work? In a succinct argument system like a zk-STARK, we have a prover and a verifier. The prover is meant to prove that the outcome of some computation gave some result, and the verifier checks the proof is correct. These two roles are analogous to the formal proof writer and the formal proof checker. In the case of this application, they coincide completely!

The prover first makes a Metamath file to prove their theorem. They then run a Metamath checker for the file as a computation inside the ZK proof system. This gives them a cryptographic output proof that they then pass to the verifier. In order to make this work, we need to be able to encode the Metamath proof checking process inside a zkVM.

This is where RISC Zero enters the picture. If we were doing this project in a zkEVM or using a circuit model, it would be necessary to write a Metamath checker in Solidity, Circom, or some other specialized language. But because RISC Zero has a zkVM for the RISC-V architecture, I can write my Metamath checker in a language like Rust. In fact, I don't even need to know Rust, because a Metamath checker written in Rust already exists, and I can just drop it into the RISC Zero VM and have it work! Even if formal methods aren't of interest to you at all, the implications for making STARK cryptography accessible are profound and exciting.

The Repository​

You can find the GitHub repository for our project here. I exaggerate a little when I say you don't even have to know Rust to make a Rust program run in the RISC zero zkVM, but not by much. The repository is a fork of the much simpler risc0/rust-starter, which has the same basic structure. There are two Rust programs in each: a host that sends data to the zkVM through the add_input() method and a guest that runs inside the zkVM, receives input via the env::read() method, and commits to outputs using the env::commit() method.

When you're designing a zk-STARK, it's good to think about what data is part of the statement and what is part of the witness. The statement is the data that is known to the verifier. In the case of our Metamath verifier, it includes the statement of the theorem that is being proven. It also includes the list of the axioms on which that theorem is based (otherwise, the prover might create their own axiom which says that the theorem is true). The witness is all the data that is known to the prover. In our case, this is simply an entire Metamath file, along with an indication of which of the theorems within that file is the one for which we are requesting the proof.

Our project has been able to run a variety of small Metamath programs, such as the one in the example above. Our primary bottleneck is the execution time within the VM; because producing a STARK proof requires memory proportional to the size of the execution trace, we can only check Metamath files of a few hundred lines before we hit the limit. The RISC Zero team has been working hard though, and I suspect we will soon have engineering solutions to remove this obstruction. From there, the only limit on the space of STARKed formal methods will be our own imaginations!

· 4 min read
Ash Schap

I am excited to announce that I have taken a new role as the Chief Strategy Officer of RISC Zero.

RISC Zero is focused on bringing the magic of Zero Knowledge Proofs to blockchains to unlock the potential of Web3 through scaling. We have built a ZKVM around the RISC-V instruction set architecture. This means the RISC Zero ZKVM can support any language that can be compiled to RISC-V, including Rust, C++, and (soon) Go. To our knowledge, this means it is the first and only ZKVM in the Web3 space that does not require developers to adopt a custom or unfamiliar language.

For those of you that know me, this may come as a surprise. I have been an Ethereum maximalist for a long time. I started my crypto journey doing business development for MakerDao, and my most recent role was Head of Growth for Uniswap, the largest and most widely used Dapp on Ethereum.

I love Ethereum. I am so proud of what we, as a community, have built. Today it is possible for users around the world to access powerful financial infrastructure in a decentralized, permissionless way. The NFT space empowers creators every day to experiment with new forms of art and new ways of engaging with their fans and collectors. There is so much that is happening on Ethereum that is groundbreaking, cutting edge and truly inspiring to watch.

But Ethereum has not yet scaled. And that has been painful at times. I started my career in crypto so optimistic that we could bring the power of smart contracts to everyone on earth, lowering the barrier to entry to Web3 and providing cheap, reliable, safe financial tools to everyone in the world who may have a need for them. But today, only the wealthy can afford to interact with Ethereum Layer 1. I didn't help build MakerDao and Uniswap so that only whales could use it. So as I took time off after leaving Uniswap last September, I started to look around and really dig into the technical forefront of the scaling question.

Layer 2 solutions like Optimism are paving the way here, and I am very excited to see the application layer maturing as those solutions gain adoption. But as I learned more about how Layer 2 works, I realized that we will never be able to build sophisticated web applications of today's Web2 without a substantial increase in throughput. Existing Layer 2 solutions will allow Web3 to grow faster and allow for the creation of more advanced applications that are far more affordable for users. But there is a cap on that throughput. As the complexity of dapps increase, that throughput will begin to max out. The only way to realistically scale blockchains is to abandon linear state and begin to experiment with parallel execution.

Zero-Knowledge Proofs can take us one step closer to that reality. My team at RISC Zero is working on a lot of clever math that makes me extremely optimistic that we can reliably scale in a parallel way without sacrificing decentralization or security, while also adding optionality for private transactions.

Our first product will be a Devnet built using Tendermint consensus, the goal being to get something into the hands of developers quickly so that we can better understand what challenges they face in building with ZKPs. Longer term, we have a lot of options on how we will deploy our products. My personal hope is that we can create an interoperable blockchain that demonstrates the power of this technology while also deploying as a Layer 2 on top of several other L1s including Ethereum and maybe even Bitcoin. Our plan is to open source everything, so my hope is that this tech will be a resource for any blockchain that needs it.

I have often said that I think I will probably spend the rest of my career trying to make the dream of global borderless money a reality. Right now this feels like the next step in that journey. I am excited to be going deeper in the stack! The magic of ZKPs has totally captured my imagination, and I searched the industry really thoroughly for the team with the right set of technical skills and the right set of ideological objectives to take this tech to the next level. RISC Zero is that team, and I could not be more thrilled to be starting this new chapter.

If you are interested in joining us, check out our careers page here:

If you want to learn more about how Zero Knowledge works, here are some resources:

And for more on RISC Zero, check these out: