Miden VM turns a program execution into a STARK proof anyone can check

The proof is the product, not the execution

Miden VM is a zero-knowledge virtual machine written in Rust. The framing in the README is the whole thing: you can execute a program on Miden VM and generate a STARK proof of its execution, and anyone can verify the proof without executing the program again or knowing its source code.

That is a different contract from running a program. An execution produces an answer; a proof produces a certificate that can be checked by a third party who has neither the program nor the inputs. For a rollup, a bridge or a computation marketplace, that difference is the entire point, and it is why the VM is designed around the proof rather than around the interpreter.

The proving system underneath is specified in the README: the prover uses the lifted STARK protocol with components from Plonky3. The workspace reflects that separation, with a lifted-air crate defining AIR traits and symbolic constraints, a lifted-stark crate implementing lifted STARK proving and verification, and a stark-transcript crate providing the transcript channels.

The division of labour inside the VM follows the same logic. The core crate defines the instruction set and shared VM types, the air crate defines the constraints checked for VM execution, the processor executes programs and builds execution traces, the prover produces STARK proofs from those traces, and the verifier verifies the proofs. The miden-vm crate provides the main library and command line interface. If you are evaluating the project, that crate list is the map of the system.

One warning in the README should shape your planning. Changes to VM internals and public interfaces can require changes in programs that use Miden VM. This is a system where the proof system and the instruction set are coupled, so an upgrade is not always a dependency bump.

Three branches track three different release promises

Until the 1.0 release, development takes place on separate branches, and the README publishes the mapping in a table. The main branch carries the minor release 0.36. The release/v0.35.1 branch carries the patch release 0.35.1. The next branch carries the major release 1.0. After the 1.0 release, main will be the release branch and next will be the development branch.

The default branch of the repository is next, which is worth knowing before you clone it. A clone of the default branch is a clone of the 1.0 development line, not of the latest published version.

The recent published versions are v0.35.0 on 2026-09-30, v0.36.0 on 2026-10-14 and v0.36.1 on 2026-10-16. The README advises using a release tag when you need a specific published version, and each branch has a CHANGELOG.md with its release history and unreleased changes.

For an adopter, the practical rule is simple and it is the rule the project is asking for. If you are building a product, pin a tag. If you are tracking the project, the next branch is where the 1.0 work is happening, and the README tells you that the internals and the public interfaces can change underneath you.

The tree also carries RELEASE-PROCEDURE.md and a tools/release-policy crate, which shows that publishing is a deliberate, scripted process rather than a manual push, and the workspace Cargo.toml carries the version 1.0.0 alongside a comment explaining that publishable crates keep their own package versions so the release tooling can publish only the crates selected for a release. In other words, the 1.0 version number is already reserved in the workspace while the published crates are still on the 0.36 line.

Procedure calls run in isolated memory with controlled kernel access

The programming model is where Miden differs from a normal virtual machine, and the README lists its capabilities precisely.

Programs can use conditional branches and loops, so control flow is not restricted. Programs can call procedures and execute them in isolated contexts with separate memory, and kernel procedures provide controlled access to the root context. That last pair of sentences is the security model in miniature. A called procedure cannot read or write the caller's memory unless it is granted access, and the way to grant it is through the kernel rather than by sharing one flat address space.

Programs can read and write memory, including local memory reserved for individual procedures, so each procedure has a private scratch area as well as the shared space it can reach through the kernel.

The arithmetic and hashing primitives are named. Programs can use native 32-bit integer operations and Eidos hashing, including Merkle path verification, and Eidos AEAD streaming. The core library includes operations on 64-bit integers and cryptographic routines, and programs can use code from external libraries.

The language is Miden Assembly, with a reference that describes the instructions and a separate assembler crate exposing parsing APIs and compilation into executable packages. The documentation at docs.miden.xyz/miden-vm covers the VM design and programming model, and the usage examples and Rust API live in the miden-vm crate.

The cost of this model is worth stating. Isolation between procedure contexts is not free, and writing an application in Miden Assembly is a commitment that goes well beyond calling a library. A team that needs a proof of a computation that can be expressed as a short program is in the target audience. A team that wants to prove an arbitrary existing application is not, and the README does not pretend otherwise.

Advice values are hints the program has to verify

Hosts can supply private inputs and computation hints through the advice provider, and the second sentence of that section is the one that matters: programs must verify advice values to establish their correctness.

This is a deliberate inversion of a common pattern. In most systems, a host is trusted and the values it provides are taken at face value. Here, the advice provider is a source of suggestions, and the program carries the burden of checking them. Anything a host supplies that the program does not verify cannot be trusted by the proof, because the proof only attests to what the program actually checked.

For a zero-knowledge system this is not optional politeness. The privacy property of the whole construction depends on the program refusing to treat unverified host input as fact, and it depends on the host being unable to see what the program is doing with those values while it runs.

The related concept is precompiles. Programs can defer computations to the host, and the VM proof commits to the deferred claims. Completing the verification requires you to also verify a precompile proof for those claims. The README points to the deferred proof lifecycle documentation for the completion and verification requirements.

So the flow for a deferred computation is two proofs rather than one. The main proof says the program asked for this computation and received this claim. The precompile proof says the claim is actually true of the inputs. A verifier that checks only the first proof has not verified the computation, and that distinction is exactly the kind of thing an integration guide should spell out before you ship.

Precompiles cover hashing, big integers and elliptic curves

The precompile side of the system is what makes it practical to do real cryptography inside a proved program.

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

That last line is the clearest statement of the design goal. Verifying a secp256k1 signature inside a zero-knowledge program is expensive to implement directly, so the work is pushed into dedicated circuits whose proofs the VM can commit to and check. The result is that a Miden program can validate a Bitcoin-style signature and have that fact attested, which is the primitive that many rollup designs need.

The recursive verification feature closes a second loop. Programs can verify VM proofs and precompile VM proofs with the core library's recursive verifiers, and the requirements for those are documented separately for sys::vm and sys::pvm. In other words, a program can check the validity of an earlier proof, which is how a chain of steps or a batch of transactions becomes one aggregated statement.

The limitations of the model are equally concrete. The set of supported algorithms is fixed at what the precompiles implement, so a program needing an algorithm outside that list has no circuit to defer to. And each precompile adds a proof obligation to the verification path, so a design that defers more work does not get cheaper verification.

Running the workspace, testing it and building for WebAssembly

The repository is a Cargo workspace with a Makefile on top of it, and the Makefile help output is the fastest map of the test surface. The workspace members listed in Cargo.toml include the VM crates, the shared field and crypto crates, the proof system crates, the precompile crates, the assembly crates and a set of benchmark crates such as blake3-bench, miden-bench, precompiles-bench, smt-codspeed and synthetic-bench.

The Makefile exposes a target per crate, which is the useful shape for continuous integration:

  make test-core                   # Test core crate

  make test-vm                     # Test miden-vm crate

Other targets listed in the same help text cover the air, assembly, crypto, processor, prover, core-lib and verifier crates, along with check-constraints, check-pvm-constants, regenerate-constraints and regenerate-pvm-constants for regenerating constraint artefacts, and a test-fast target described as fast tests.

For WebAssembly, the README is specific. Miden VM supports WebAssembly builds without Rust's standard library, and the supported no_std targets are wasm32-unknown-unknown and wasm32-wasip1, which require Cargo's --no-default-features flag. The workspace Cargo configuration enables SIMD128 instructions for wasm32-unknown-unknown with -C target-feature=+simd128, and these instructions accelerate hashing in the Plonky3 backend.

That last point has a trap in it, and the README flags it. Cargo applies the configuration only when you build from this workspace or a directory inside it. When you use Miden VM as a dependency, you have to set the same flag in your own Cargo configuration or in RUSTFLAGS. Miss it and your WebAssembly build simply runs without the SIMD path, with no error to tell you.

For proof generation, the concurrent feature generates STARK proofs with multiple threads, using Rayon for parallel computation, and RAYON_NUM_THREADS controls the number of worker threads. The processor APIs let developers step through execution and retain source locations, including for inlined calls, and programs can print VM state through the core library's debug procedures, which is the debugging story in a proved environment where a stack trace is not available.

Dual licensing, a pinned Rust toolchain, and repository-level checks

The workspace package metadata sets license to MIT OR Apache-2.0, and the repository carries both LICENSE-MIT and LICENSE-APACHE, with the README badges showing the same pair. That is the standard Rust dual licence, and the choice between them is a decision for whoever owns licence compliance in your organisation, since the two sets of obligations differ. Nothing here is legal advice, and the licence files in the repository are the text to read.

The toolchain is pinned rather than floating. The Cargo configuration sets rust-version to 1.96.1, the README badge names the same compiler version, and a rust-toolchain.toml sits at the root of the tree alongside a rustfmt.toml and a .clippy.toml. The edition is 2024, and the resolver is set to 3. For a project on a pre-1.0 line, pinning the compiler is what keeps a build reproducible across contributors.

The repository also carries the tooling that a project of this size needs, and their presence says more about its engineering process than the feature list does. There is a deny.toml, which is the configuration for cargo-deny and therefore for licence and vulnerability checks on dependencies, a zizmor.yml for scanning GitHub Actions workflows, a lychee.toml for link checking, bench-baselines for comparing benchmark results over time, and a tools/release-policy crate. Alongside them sit SECURITY.md, CONTRIBUTING.md, CHANGELOG.md, RELEASE-PROCEDURE.md and a .github directory with test and build workflows.

The last push was on 2026-10-20, and the repository is not archived, so the code is being worked on. The 1.0 release is still in development on the next branch, and the README is explicit that VM internals and public interfaces can change under programs that depend on them, so the upgrade path from 0.36 to 1.0 is a migration rather than a version bump.

Editorial conclusion

Miden VM fits a team that needs to prove a computation ran correctly without revealing the program or the inputs, and it fits developers willing to work in Miden Assembly rather than an existing language, since the WebAssembly and no_std support covers hosting rather than authoring. It is the wrong tool for a project that only needs to run code, because the fast processor and processor APIs already cover that case and the proof machinery is where the cost and the complexity live. Before you build on it, pin a release tag rather than a branch, because the README states that changes to VM internals and public interfaces can require changes in programs that use Miden VM, and read the recursive verifier requirements in sys::vm and sys::pvm before assuming a proof can be checked inside the VM.

Frequently asked questions

Official sources

1. 0xMiden/miden-vm on GitHub
2. License: Apache-2.0
3. Project website
4. README
5. Releases