Miden Virtual Machine

Miden VM is a zero-knowledge virtual machine written in Rust.

Overview

You can execute a program on Miden VM and generate a STARK proof of its execution. Anyone can verify the proof without executing the program again or knowing its source code.

The prover uses the lifted STARK protocol with components from Plonky3.

For usage examples and the Rust API, see the miden-vm crate. The documentation covers the VM design and programming model.

Branches and releases

Until the 1.0 release, development takes place on the following branches:

After the 1.0 release, main will be the release branch and next will be the development branch. Use a release tag when you need a specific published version.

Changes to VM internals and public interfaces can require changes in programs that use Miden VM. Each branch has a CHANGELOG.md with its release history and unreleased changes. See Contributing for the contribution workflow.

Features

Miden VM supports general computation and proof generation with the following capabilities.

Programming model

• Programs can use conditional branches and loops.
• Programs can call procedures and execute them in isolated contexts with separate memory. Kernel procedures provide controlled access to the root context.
• Programs can read and write memory, including local memory reserved for individual procedures.
• Programs can use native 32-bit integer operations and Poseidon2 hashing, including Merkle path verification.
• Programs can use code from external libraries. The core library includes operations on 64-bit integers and cryptographic routines.

Miden Assembly is the language for Miden VM programs. The assembly reference describes the instructions. See the assembler documentation for parsing APIs and compilation into executable packages.

Hosts and private inputs

Hosts can supply private inputs and computation hints through the advice provider. Programs must verify advice values to establish their correctness.

Precompiles

Programs can defer computations to the host. The VM proof commits to the deferred claims. To complete verification, you must also verify a precompile proof for those claims. See the deferred proof lifecycle for completion and verification requirements.

The precompile VM proves deferred claims with specialized circuits. The current precompiles support Keccak-256 hashing, 256-bit integer arithmetic, and elliptic curve operations. The core library uses these operations for secp256k1 ECDSA verification and public key recovery.

Recursive verification

Programs can verify VM proofs and precompile VM proofs with the core library's recursive verifiers. See sys::vm and sys::pvm for their requirements.

Execution and platforms

You can use the fast processor to execute programs without generating a proof. Developers can use processor APIs to step through execution and retain source locations, including inlined calls. Programs can also print VM state through the core library's debug procedures.

Miden VM supports WebAssembly builds without Rust's standard library (no_std). The supported no_std targets are wasm32-unknown-unknown and wasm32-wasip1. Use Cargo's --no-default-features flag for these builds.

The workspace Cargo configuration enables SIMD128 instructions for wasm32-unknown-unknown with -C target-feature=+simd128. These instructions accelerate hashing in the Plonky3 backend. Cargo applies this configuration only when you build from this workspace or a directory inside it. When you use Miden VM as a dependency, set the same flag in your own Cargo configuration or RUSTFLAGS.

Enable the concurrent feature to generate STARK proofs with multiple threads. The prover uses Rayon for parallel computation. Set RAYON_NUM_THREADS to control the number of worker threads. See the benchmarks for measured performance.

Project structure

The workspace contains the main crates below. Internal support and benchmark crates are omitted.

Documentation

The miden-docs repository imports the Markdown from docs/src for the published documentation website. You can build a local preview with Docusaurus. See the docs setup instructions.

Performance

The benchmarks below should be viewed only as a rough guide for expected future performance. The reasons that many optimizations have not been applied yet, and we expect that there will be some speedup once we dedicate some time to performance optimizations.

A few general notes on performance:

• Execution time is dominated by proof generation time. In fact, the time needed to run the program is usually under 0.01% of the time needed to generate the proof.
• Proof verification time is really fast. In most cases it is under 1 ms, but sometimes gets as high as 2 ms or 3 ms.
• Proof generation process is dynamically adjustable. In general, there is a trade-off between execution time, proof size, and security level (i.e. for a given security level, we can reduce proof size by increasing execution time, up to a point).
• Both proof generation and proof verification times are greatly influenced by the hash function used in the STARK protocol. In the benchmarks below, we use BLAKE3, which is a really fast hash function.

To refresh the Blake3 results below, run the same Criterion benchmark used by CI:

RAYON_NUM_THREADS=16 cargo run --profile optimized -p miden-vm-blake3-bench --bin blake3-nonregression -- run \
  --repo-root . \
  --output-dir target/blake3-nonregression \
  --rayon-num-threads 16 \
  --sample-size 10 \
  --light-sample-size 100 \
  --measurement-time-secs 1 \
  --warm-up-time-secs 1 \
  --bench-axes all \
  --git-ref "$(git rev-parse HEAD)"

The result is written to target/blake3-nonregression/result.json; the harness does not parse the miden-vm run or miden-vm prove text output. The benchmark records execute_for_proving_sync, build_trace, prove_trace_sync, and e2e_prove. It also accepts the historical execute_trace_inputs_sync axis input, normalizing both spellings to the stable execute_for_proving_sync metric key. The e2e_prove metric runs execution and trace generation on each sample, but only measures the prover span. The harness also proves and verifies the program once before timing proof-heavy axes.

Single-core prover performance

When executed on a single CPU core, the current version of Miden VM operates at around 20 - 25 KHz. In the benchmarks below, the VM executes a Blake3 example program on Apple M4 Max CPU in a single thread. The generated proofs have a target security level of 96 bits.

As can be seen from the above, proving time roughly doubles with every doubling in the number of cycles, but proof size grows much slower.

Multi-core prover performance

STARK proof generation is massively parallelizable. Thus, by taking advantage of multiple CPU cores we can dramatically reduce proof generation time. For example, when executed on an 16-core CPU (Apple M4 Max), the current version of Miden VM operates at around 170 KHz. And when executed on a 64-core CPU (Amazon Graviton 4), the VM operates at around 200 KHz.

In the benchmarks below, the VM executes the same Blake3 example program for 220 cycles at 96-bit target security level:

Recursion-friendly proofs

Proofs in the above benchmarks are generated using BLAKE3 hash function. While this hash function is very fast, it is not very efficient to execute in Miden VM. Thus, proofs generated using BLAKE3 are not well-suited for recursive proof verification. To support efficient recursive proofs, we need to use an arithmetization-friendly hash function. Miden VM natively supports Poseidon2, which is one such hash function. One of the downsides of arithmetization-friendly hash functions is that they are noticeably slower than regular hash functions.

In the benchmarks below we execute the same Blake3 example program for 220 cycles at 96-bit target security level using Poseidon2 hash function instead of BLAKE3:

References

Miden VM uses STARK proofs to establish that a computation was executed correctly. Eli Ben-Sasson and Michael Riabzev developed STARKs with their coauthors at Technion (Israel Institute of Technology). STARKs require no trusted setup and rely on few cryptographic assumptions.

Here are some resources to learn more about STARKs:

• STARKs whitepaper: Scalable, transparent, and post-quantum secure computational integrity
• STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs

Vitalik Buterin's blog series on zk-STARKs:

• STARKs, part 1: Proofs with Polynomials
• STARKs, part 2: Thank Goodness it's FRI-day
• STARKs, part 3: Into the Weeds

Alan Szepieniec's STARK tutorials:

• Anatomy of a STARK
• BrainSTARK

StarkWare's STARK Math blog series:

• STARK Math: The Journey Begins
• Arithmetization I
• Arithmetization II
• Low Degree Testing
• A Framework for Efficient STARKs

StarkWare's STARK tutorial:

• STARK 101

Licensing

Any contribution intentionally submitted for inclusion in this repository, as defined in the Apache-2.0 license, shall be dual licensed under the MIT and Apache 2.0 licenses, without any additional terms or conditions.