The Nexus zkVM is steadily evolving, with each release introducing incremental improvements in functionality and performance — all while maintaining a strong focus on security.

Development of a new version starts with a formal specification, which serves as the foundation for the code. This document outlines how instruction execution, register and memory access are constrained, and how different components of the zkVM interact.

zkVM 3.0 and Beyond: Toward Modular, Distributed Zero-Knowledge Proofs

In March, we released the zkVM 3.0, this post goes into more detail about its design intent and features. The landscape of zero-knowledge virtual machines (zkVMs) is evolving quickly, driven by the demand for scalable, efficient, and reliable systems that can prove the correct execution of arbitrary programs regardless

NexusMichel Abdalla

Adhering to the specification in the implementation is one of our key principles, it facilitates future maintenance and extensions of the prover, and makes the codebase easier to review and audit.

With this goal in mind, Nexus zkVM 3.0 uses a thin-layer framework on top of S-two. It helps eliminate repetitive code and enables defining components in isolation. But what’s most relevant here is how it handles constraints — the description of a component’s circuit.

A closer look at circuit definitions

Let’s consider a simple example — Load Upper Immediate (LUI). This instruction loads a zero-extended immediate into rd, and is constrained in the code as follows:

let value_a = trace_eval!(trace_eval, ValueA);
let value_c = trace_eval!(trace_eval, ValueC);
let [is_lui] = trace_eval!(trace_eval, Column::IsLui);

// Setting a_val = c_val
// is_lui・(c_val_1 - a_val_1) = 0
// is_lui・(c_val_2 - a_val_2) = 0
// is_lui・(c_val_3 - a_val_3) = 0
// is_lui・(c_val_4 - a_val_4) = 0
for i in 0..WORD_SIZE {
    eval.add_constraint(is_lui.clone() * (value_c[i].clone() - value_a[i].clone()));
}

The overall pattern is consistent across the codebase — each constraint is annotated with a doc comment that directly reflects the corresponding line in the specification.

While this is one of the simplest examples, most components are significantly more complex. Take a look at how load and store instructions are defined here.

The acceleration phase

The zkVM architecture is currently undergoing significant changes, which means the process of specifying constraints must be repeated. One valid approach would be to invest time in building a parser that processes component definitions directly from the specification and generates code. But there’s an even faster — and more flexible — alternative: AI.

All it takes is defining a series of prompts — the model, with the full codebase already indexed, effectively acts as a parser.

Take the clock increment logic, with a selector for padding rows, as an input:

• (1 − is-local-pad) · (clk-next(1) + clk-next(2) · 2^8 
    + clk-carry(1) · 2^16 − clk(1) − clk(2) · 2^8 − 1) = 0
• (1 − is-local-pad) · (clk-next(3) + clk-next(4) · 2^8 
    + clk-carry(2) · 2^16 − clk(3) − clk(4) · 2^8 − clk-carry(1)) = 0

Thanks to how well AI models follow patterns, it was able to generate the corresponding code with ease:

let clk = trace_eval!(trace_eval, Clk);
let clk_next = trace_eval!(trace_eval, ClkNext);
let clk_carry = trace_eval!(trace_eval, ClkCarry);
let is_local_pad = trace_eval!(trace_eval, IsLocalPad);
let modulus = E::F::from(256u32.into());

// Clock increment constraints
// First limb pair
// (1 − is-local-pad) · (clk-next(1) + clk-next(2) · 2^8 + clk-carry(1) · 2^16 − clk(1) − clk(2) · 2^8 − 1) = 0
eval.add_constraint(
    (E::F::one() - is_local_pad.clone()) * (
        clk_next[0].clone() + clk_next[1].clone() * modulus.clone() +
        clk_carry[0].clone() * modulus.clone().pow(2) -
        clk[0].clone() - clk[1].clone() * modulus.clone() - E::F::one()
    )
);

// Second limb pair
// (1 − is-local-pad) · (clk-next(3) + clk-next(4) · 2^8 + clk-carry(2) · 2^16 − clk(3) − clk(4) · 2^8 − clk-carry(1)) = 0
eval.add_constraint(
    (E::F::one() - is_local_pad.clone()) * (
        clk_next[2].clone() + clk_next[3].clone() * modulus.clone() +
        clk_carry[1].clone() * modulus.clone().pow(2) -
        clk[2].clone() - clk[3].clone() * modulus.clone() - clk_carry[0].clone()
    )
);

AI isn’t confined to simple cases — it scales naturally to more complex components, such as the previously mentioned load and store instructions. Moreover, it can even reverse the process: taking code and generating the corresponding constraint expression, or suggesting LaTeX updates to the spec when inconsistencies arise.

Did it get the code right?

AI-generated code should still undergo manual review by other engineers, just as it did during the development of zkVM 3.0. As a bonus, this workflow naturally encourages a test-driven development (TDD) approach.

A second AI model can serve as an automated reviewer — flagging inconsistencies and checking against the spec, all while giving your human reviewer one less reason to postpone their coffee break.

What’s next?

The path forward is clear: as circuits grow in complexity, AI tooling will go beyond writing constraints — assisting with components and LogUp traces generation, and perhaps even guiding new instruction design. We’re just scratching the surface.