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 Eidos hashing, including Merkle path verification.
• Programs can use Eidos AEAD streaming.
• 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 precompiles support Keccak-256, SHA-256 and SHA-512 hashing. They also support 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

These benchmarks use Eidos, Miden VM's native hash function, for STARK proof generation. The resulting proofs are therefore recursion-friendly: they can be efficiently verified inside Miden VM.

Execution measures the fast interpreter; proving includes trace generation after witness construction. RAM consumed is peak process memory. See the performance guide.

To reproduce the multi-core results:

cargo build --locked --profile optimized -p miden-vm-blake3-bench --bin vm-performance
target/optimized/vm-performance --hash eidos --threads 14 --iterations 128 --samples 5

Single-core prover performance

The VM executes the Blake3 example program on an Apple M4 Pro with one Rayon worker. The rows measure chains of 2, 8, 32, and 128 Blake3 calls, with VM cycles padded to a power of two. The default proof parameters target 96-bit conjectured security. See the Eidos security and usage guide.

The Apple M5 Max results use one Rayon worker. Timings and proof sizes are medians of five samples after one warmup proof.

The AMD Ryzen 9 9950X results use one Rayon worker. Ryzen timings and proof sizes are medians of five samples.

Multi-core prover performance

The following runs use 128 Blake3 calls (828,632 VM cycles, padded to 2²⁰).

Execution % is execution time divided by proving time. Implied frequency is the padded VM cycle count (2²⁰ for these runs) divided by proving time, reported in KHz.

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:

• 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.