Use Case: Program Execution

​

Introduction

As this walkthrough describes a more advanced use case for the zkVM, we recommend reviewing both the SDK Quick Start and the simpler Stable Matching walkthrough first.

By design, a zkVM proves the correctness of a program’s execution. However, a more advanced use case arises when the program to be proven is not the code running directly in the zkVM, but is instead provided as input to the zkVM. In this case, the zkVM executes an interpreter as its guest program, which then reads, interprets, and runs the input program inside the zkVM. This effectively allows the zkVM to generate a proof for the execution of arbitrary, dynamically supplied programs.

Consider the following guest program in which program_to_be_proven is nested inside as input to the zkVM

fn digest(program: &ElfFile) -> Vec<u8> { ... }

fn rv32i_interpret(program: &ElfFile) -> Vec<u8> { ... }

#[nexus_rt::main]
#[nexus_rt::private_input(program_to_be_proven)]
#[nexus_rt::public_input(program_digest)]
fn main(program_to_be_proven: ElfFile, program_digest: Vec<u8>) -> Vec<u8> {
    assert_eq!(digest(&program_to_be_proven), &program_digest);

    nexus_rt::print!("Program digest {} validated, executing program... ", program_digest);

    let output = rv32i_interpret(&program_to_be_proven);

    nexus_rt::println!("completed.");

    output
}

At first glance, this pattern may seem redundant—why not just run program_to_be_proven directly as the guest program? However, this level of indirection unlocks powerful capabilities that significantly expand the utility of the zkVM.

​

Enabling Private Program Execution

The first benefit, illustrated by the example above, is the ability to treat the program to be proven as a private input. This allows the zkVM to prove the execution of programs without revealing their source, making it possible to build private smart contracts on-chain.

By comparing the program’s digest to a public input, verifiers can still check meaningful properties — such as:

• Consistency of the private program across multiple invocations
• Conformance to a known, audited version without exposing implementation details

This digest check enables trust minimization while preserving privacy.

​

Generalization Across Programs with a Single zkVM Binary

A second, more technical benefit is that this structure enables the zkVM to handle a wide range of programs through a single, fixed guest binary — the interpreter.

With careful planning around memory constraints (e.g. stack, heap, and output size bounds), this pattern allows:

• Shared proving key / public parameter reuse across many programs, which can simplify definitions for non-transparent provers which may require per-program setup
• Simplified deployment pipelines for applications/smart contracts verifying zkVM proofs on-chain
• Easier management of systems using non-transparent proving systems, which often require per-program setup (though note: the Stwo prover used here is transparent)_

This approach decouples the proving circuit from individual guest programs, significantly improving composability and maintainability.

​

The Lambda Calculus Model

Instead of working through this design at the full complexity of the RISC-V32i instruction set, we will work through a simpler example of the core concept using a much more fundamental computational model: the lambda calculus.

​

Implementation

To start, we will follow along with the SDK Quick Start. After installing the zkVM, we run:

$ cargo nexus host lambda_calculus

to initialize the host and guest programs. We begin by creating a shared library for the guest and host program, which we’ll locate within the guest program crate.

​

Shared Library

The first part of the library will define terms in the calculus:

#![cfg_attr(no_std)]

extern crate alloc;

use alloc::boxed::Box;
use core::fmt::{Debug, Display};
use serde::{Serialize, Deserialize};

#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[repr(transparent)]
pub struct DeBruijnIndex(usize);

impl From<usize> for DeBruijnIndex {
    fn from(value: usize) -> Self {
        Self(value)
    }
}

impl Display for DeBruijnIndex {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}", self.0)
    }
}

#[derive(Clone, Debug, Serialize, Deserialize)]
enum Term<R> {
    Var(DeBruijnIndex),
    Lambda(R),
    Apply(R, R),
}

impl<R: Display> Display for Term<R> {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        match self {
            Term::Var(v) => write!(f, "{v}"),
            Term::Lambda(t) => {
                write!(f, "(\\")?;
                write!(f, "{t}")?;
                write!(f, ")")
            }
            Term::Apply(t1, t2) => {
                write!(f, "(")?;
                write!(f, "{t1}")?;
                write!(f, " ")?;
                write!(f, "{t2}")?;
                write!(f, ")")
            }
        }
    }
}

This code block defines an Enum of the possible Terms available: an indexed Var, a Lambda function definition, and an Apply function application, as well as some useful trait implementations for constructing and debugging. In the rest of the library, we’ll define full expressions in the calculus, which amount to programs that are “executed” via reduction.

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Expr(Term<Box<Self>>);

impl Display for Expr {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl PartialEq for Expr {
    fn eq(&self, other: &Self) -> bool {
        self.clone().eval().structural_eq(&other.clone().eval())
    }
}

impl Eq for Expr {}

impl Expr {
    pub fn var<T: Into<DeBruijnIndex>>(binding: T) -> Self {
        Self(Term::Var(binding.into()))
    }

    pub fn lambda<T: Into<Box<Self>>>(inner: T) -> Self {
        Self(Term::Lambda(inner.into()))
    }

    pub fn apply<T1, T2>(left: T1, right: T2) -> Self
    where
        T1: Into<Box<Self>>,
        T2: Into<Box<Self>>,
    {
        Self(Term::Apply(left.into(), right.into()))
    }

    pub fn identity() -> Self {
        Self::lambda(Self::var(0))
    }

    pub fn omega() -> Self {
        let expr = Self::lambda(Self::apply(Self::var(0), Self::var(0)));
        Self::apply(expr.clone(), expr)
    }

    pub fn step(&self) -> Self {
        fn subst(body: Expr, arg: Expr, depth: usize) -> Expr {
            match body.0 {
                Term::Var(i) => {
                    if i.0 == depth {
                        arg
                    } else {
                        Expr::var(i)
                    }
                }
                Term::Lambda(e) => subst(*e, arg, depth + 1),
                Term::Apply(e1, e2) => {
                    Expr::apply(subst(*e1, arg.clone(), depth), subst(*e2, arg, depth))
                }
            }
        }

        // attempt beta reduction
        if let Term::Apply(e1, e2) = &self.0 {
            if let Term::Lambda(e) = &e1.0 {
                return subst(*e.clone(), *e2.clone(), 0);
            }
        }

        self.clone()
    }

    pub fn structural_eq(&self, other: &Self) -> bool {
        match (&self.0, &other.0) {
            (Term::Var(i), Term::Var(j)) => *i == *j,
            (Term::Lambda(e), Term::Lambda(f)) => e.structural_eq(f),
            (Term::Apply(e1, e2), Term::Apply(f1, f2)) => {
                e1.structural_eq(f1) && e2.structural_eq(f2)
            }
            _ => false,
        }
    }

    pub fn eval(self) -> Self {
        let mut curr = self;
        loop {
            let next = curr.step();
            if next.structural_eq(&curr) {
                return curr.clone();
            } else {
                curr = next;
            }
        }
    }
}

The implementation also includes various trait implementations as well as both individual step and iterative eval routines that reduce the statement into a stable form.

In order to make our common library work across both the host and guest, we have a few quick steps we need to handle. First, we need to update the guest crate to depend on serde, which the library uses for serializing and deserializing the Expr structs to and from the zkVM:

...

[dependencies]
nexus-rt = { git = "https://github.com/nexus-xyz/nexus-zkvm.git", tag = "0.3.0", version = "0.3.0" }
postcard = { version = "1.1.1", default-features = false, features = ["alloc"] }
serde = { version = "1.0", default-features = false, features = ["derive"] }

...

Next, we need to export the common code as a Rust library.

#![no_std]

pub mod common;
pub use common::*;

And lastly we need to make this library visible to the host program.

...

[dependencies]
nexus-sdk = { git = "https://github.com/nexus-xyz/nexus-zkvm.git", tag = "0.3.0", version = "0.3.0" }
guest = { path = "./src/guest" }

...

​

Guest Program

Returning to the guest program, as an Expr is a program in the lambda calculus, we can now implement our (dead simple) interpreter — for simplicity, we omit any hash-based consistency checking:

#![cfg_attr(target_arch = "riscv32", no_std, no_main)]

use guest::Expr;

#[nexus_rt::main]
#[nexus_rt::private_input(program_to_be_proven)]
fn main(program_to_be_proven: Expr) -> Expr {
    program_to_be_proven.eval()
}

​

Host Program

Here we create a suitable host program that invokes the guest using the private program:

use nexus_sdk::{
    compile::{cargo::CargoPackager, Compile, Compiler},
    stwo::seq::Stwo,
    ByGuestCompilation, Local, Prover, Viewable,
};

use guest::Expr;

const PACKAGE: &str = "guest";

fn main() {
    println!("Compiling guest program...");
    let mut prover_compiler = Compiler::<CargoPackager>::new(PACKAGE);
    let prover: Stwo<Local> =
        Stwo::compile(&mut prover_compiler).expect("failed to compile guest program");

    let program_to_be_proven = Expr::apply(Expr::identity(), Expr::var(42));

    println!("Proving execution of vm...");
    let (view, proof) = prover.prove_with_input::<Expr, ()>(
        &program_to_be_proven,
        (),
    ).expect("failed to prove program");

    assert_eq!(view.exit_code().expect("failed to retrieve exit code"), nexus_sdk::KnownExitCodes::ExitSuccess as u32);

    let output = view.public_output::<Expr>().expect("failed to retrieve public output");

    println!("Reduced expression: {}", output);
}

​

Verification

Meanwhile, as desired verification does not require any access to the private program:

println!("Verifier recompiling guest program...");
let mut verifier_compiler = Compiler::<CargoPackager>::new(PACKAGE);
let path = verifier_compiler.build().expect("failed to (re)compile guest program");

print!("Verifying execution...");
proof.verify_expected_from_program_path::<&str, (), Expr>(
  &(),                                           // at view.public_input
  nexus_sdk::KnownExitCodes::ExitSuccess as u32, // at view.exit_code
  &output,                                       // at view.public_output
  &path,                                         // path to program binary
  &[]                                            // no associated data,
).expect("failed to verify proof");

In this way, we are able to use the zkVM to prove the correctness of executing a private program.

​

Conclusion

Through this walkthrough, we have successfully demonstrated how the Nexus zkVM can be applied to fundamental computational models, showcasing its versatility beyond practical applications. We accomplished our goal of proving the correct execution of lambda calculus programs while keeping the program logic completely private.

The key achievements of this implementation include: (1) a shared library architecture that enables code reuse between guest and host programs, (2) a clean abstraction for lambda calculus expressions with evaluation semantics, (3) a zkVM-based interpreter that generates proofs for program execution, and (4) a verification system that confirms correctness without exposing the original program.

This lambda calculus example illustrates several important principles about zkVM applications.

First, it demonstrates that zkVMs can handle abstract computational models, not just concrete algorithms. The ability to prove correct evaluation of lambda expressions opens possibilities for verifying functional programming languages, theorem provers, and symbolic computation systems.

Second, this walkthrough shows how the same privacy-preserving verification principles from our stable matching example apply to entirely different domains. Whether proving the correctness of medical residency assignments or lambda calculus reductions, the zkVM provides the same fundamental guarantee: mathematical proof of correct execution without revealing sensitive inputs.

Finally, the simplicity of this implementation—requiring just a few dozen lines of code—highlights how accessible zkVM technology has become for researchers and developers. Complex theoretical concepts like lambda calculus evaluation can be made verifiable with minimal overhead, enabling new possibilities for transparent yet private computation in academic research, compiler verification, and programming language development.

This approach transforms program execution from a “trust the interpreter” model to a “verify the computation” model, providing mathematical assurance that programs are evaluated correctly according to their formal semantics. The same principles demonstrated here extend to any computational model where execution correctness matters but program privacy must be preserved.