ZK/SEC Research notes from zkSecurity
All posts
Jolt · Part 4 of 4

Breaking Jolt’s Verifier with an Unbound Uni-Skip Claim

I found a soundness bug in Jolt’s transparent/non-ZK verifier that allowed a forged proof to verify for an execution that never actually happened (X post).

The issue was fixed quickly in PR #1474 after I disclosed it privately.

At a high level, the verifier trusted a proof-provided intermediate claim without checking that it was actually produced by the previous polynomial message. That missing equality was enough to let a malicious prover splice together two locally consistent proof components into one globally false proof.

Bug Summary

Jolt’s uni-skip verifier accepted a proof-provided output claim without checking that it matched the submitted univariate polynomial evaluated at the verifier’s challenge.

The missing check was essentially:

claimed_output == uni_poly.evaluate(r0)

where r0 is the Fiat–Shamir challenge sampled after the first-round univariate polynomial.

Without this check, the first-round uni-skip proof and the remainder proof could each look valid while silently referring to different statements.

In other words, the verifier checked both sides of the bridge, but forgot to check that the bridge itself was connected.

What Uni-Skip Is

Uni-skip is a prover-side optimization for sumcheck. The paper Speeding Up Sum-Check Proving describes it as an optimization that modifies the protocol by replacing part of the usual sumcheck flow with a higher-degree univariate step. In Jolt, this is used as part of the optimized Spartan prover path.

In an ordinary sumcheck, the prover reduces a large multilinear claim one variable at a time. After the prover sends a univariate polynomial for the current round, the verifier samples a challenge r, evaluates that polynomial at r, and uses the result as the next claim.

Uni-skip compresses some of that work. Instead of walking through several small Boolean rounds in the usual way, the prover sends a larger univariate polynomial that represents a packed slice of the computation. The verifier then samples a challenge r0, and the protocol continues with a remainder sumcheck from the value of that univariate polynomial at r0.

Constraints

Uni-skip changes how the first part of the sumcheck is represented, but it does not change what the verifier must learn from it: after sampling r0, the verifier must use the submitted univariate polynomial evaluated at r0 as the next claim for the remainder sumcheck.

In this bug, the verifier checked that the submitted univariate polynomial had the correct total sum, and it also checked the remainder proof starting from a claimed output value. But it passed to check that the claimed output value was actually the polynomial evaluated at r0.

That missing check is the entire bug:

claimed_output == uni_poly.evaluate(r0)

The Two Affected Uni-Skip Paths

There were two relevant uni-skip paths:

SpartanOuter
SpartanProductVirtualization

Both had the same missing boundary check, but they sit in different parts of the verifier.

α_outer

α_outer is the output claim of the SpartanOuter uni-skip path.

It becomes the input claim to the Stage 1 outer remainder sumcheck.

Stage 1:
  SpartanOuter uni-skip
      -> α_outer
  SpartanOuter remainder
      -> input claim = α_outer

This path is especially important because SpartanOuter is where Jolt’s outer R1CS layer checks VM execution semantics: instruction behavior, register values, RAM accesses, store/load consistency, and related constraints.

So if a forged proof can arrange for the only remaining mismatch to be an execution-semantics violation, that mismatch naturally lands in Stage 1.

α_product

α_product is the output claim of the SpartanProductVirtualization uni-skip path.

It goes into Stage 2, but not as the whole Stage 2 claim. Stage 2 batches several sumcheck instances together:

Stage 2:
  0. RAM read/write checking
  1. Spartan product remainder        <- input claim = α_product
  2. instruction lookup claim reduction
  3. RAM RAF evaluation
  4. public output check

So α_product is specifically the input claim for the Spartan product remainder instance inside Stage 2.

This path is about product-virtualization constraints. It is affected by the same missing binding check, but it was not the most direct route for my false-output PoC.

Why the PoC Uses α_outer

For the PoC, I targeted the return-value path instead of only changing the public output.

The guest returns its input, so the value appears in the CPU trace and is written through the return/output path. By modifying the CPU-side witness generation around that path, I could make the verifier-facing proof state correspond to the forged output.

That does not make the execution valid. It only moves the remaining inconsistency into the outer execution constraints, which are enforced by SpartanOuter.

This is exactly where α_outer matters.

The forged proof leaves the final lie at the Stage 1 outer-R1CS boundary, then relies on the missing binding check to decouple the outer first-round polynomial from the outer remainder proof.

The result is a proof whose pieces are locally consistent, but whose execution claim is globally false.

Impact

The impact is verifier soundness failure in the transparent/non-ZK path: the verifier can accept a public output that the guest program did not produce.

In the minimal PoC, the guest program returns its input unchanged. For input 1333337, the valid output should be 1333337, but the unpatched verifier accepts a proof claiming 1333338.

#![cfg_attr(feature = "guest", no_std)]

#[jolt::provable(heap_size = 128, max_trace_length = 1024)]
fn return_same(x: u64) -> u64 {
    x
}
input:              1333337
valid output:       1333337
claimed output:     1333338
unpatched verifier: accepts
patched verifier:   rejects

That is the core failure mode of a zkVM soundness bug: the verifier accepts a public output that the guest program did not produce.

Patch

The fix is conceptually simple: after sampling r0, compare the proof-provided output claim with the actual evaluation of the submitted univariate polynomial.

let expected_output = proof.uni_poly.evaluate(&r0);
let claimed_output =
    sumcheck_instance.expected_output_claim(opening_accumulator, &[r0]);

if claimed_output != expected_output {
    return Err(ProofVerifyError::UniSkipVerificationError);
}

The important part is that this check happens before the claimed output is used as the input claim for the remainder proof.

PoC

See more details and a working PoC at jolt-uni-skip-exploit.

Thanks to young (coo) for cheering me on during the hunt.

Keep reading
Recommended

Improving the Security of the Jolt zkVM

We recently explored a16z’s Jolt zkVM to bolster its security, discovering significant bugs in the process. Our findings revealed vulnerabilities that could allow malicious provers to forge proofs, highlighting the crucial role of manual reviews in catching these issues. Jolt, with its unique approach using the Lasso lookup technique, aims to improve prover efficiency and system scalability. With these bugs now fixed, this work underscores the importance of thorough audits in ensuring the reliability of advanced zkVM technology. Stay tuned as we continue to delve into zkVM security insights.

Suneal Gong, Imam Al-Fath · November 19, 2024

A challenge on the Jolt zkVM

Last weekend, we had a blast crafting challenges for a CTF event at the MOCA Italian hacker camp. One cryptography challenge, "2+2=5," involved the Jolt zkVM and a RISC-V program. In this post, we share the ins and outs of the challenge, the clever use of a modified Jolt library, and how we managed to prove an invalid execution without triggering verification alarms. Get ready to dive into the world of Jolt and pick up some nifty insights on exploiting cryptographic systems like a true hacker.

Giorgio Dell'Immagine · September 24, 2024

Cryptography challenges @KalmarCTF 2026

Minsun shares a high-level overview of the hard cryptography challenges he authored for KalmarCTF 2026, focusing on the broader ideas behind their design and solutions. The post reflects on how subtle randomness failures and algebraic structure can lead to deep vulnerabilities.

Minsun Kim · April 28, 2026
More to explore

Unveiling the Magic Behind Starknet: A Deep Dive into New Specifications

In our deep dive into Starknet's cryptographic components, we tackled the challenge of missing comprehensive specifications by reverse-engineering and publishing draft specs. Readers can explore our work on key protocols like Starknet Channels and STARK Verifier, with an open invitation to join us in refining these efforts. Curious to see what we've pieced together? Check out our drafts and get involved!

David Wong · November 15, 2024

Uncovering and Fixing an Inflation Bug in Aleo

In November 2024, we found a significant inflation bug in the Aleo mainnet that could have allowed token minting without proper checks. We immediately informed the Aleo team, who swiftly addressed the issue with no detected exploitation. This post dives into the inner workings of Aleo and explains how transitions and records operate, providing insight into how the vulnerability was discovered and resolved. It's an intriguing look at blockchain security, zero-knowledge proofs, and the importance of thorough type checks to ensure robust protocol integrity.

Suneal Gong · February 19, 2025

wasmati: You should write your WebAssembly in TypeScript

If you're into WebAssembly (Wasm) and want to speed up your JavaScript, this blog post is for you! We talk about our journey with Wasm and how we created a TypeScript library called wasmati that lets you write Wasm at the instruction level. You'll get the inside scoop on how this can significantly improve performance, especially for cryptography work. Plus, we showcase a real-world example comparing Wasm and JS bigint performance, proving that Wasm can be over four times faster. Dive in to see how we've combined the flexibility of TypeScript with the power of Wasm for high-performance coding.

Gregor Mitscha-Baude · June 02, 2023