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
Latest

Optimizing Cryptography with AI

Many of us are using AI to generate code. Vibe coding cryptography is especially sensitive - you have to uphold strict mathematical correctness. This can lead to wrong security guarantees and soundness bugs. We will discuss what are some patterns to do it well.

Kobi Gurkan · August 11, 2026

Introducing zkvmBlast: Differential Fuzzing for Ethereum's zkVMs

zkVMs are moving to the center of Ethereum's roadmap, which means a bug in a zkVM is turning into a bug in Ethereum itself. We built zkvmBlast, a zkVM-agnostic differential fuzzer that runs the same program across SP1, RISC0, OpenVM, Pico, Zisk, and Airbender against a reference simulator and flags any disagreement. It hunts for both soundness and completeness bugs, with a deliberate focus on completeness, an under-explored class that can turn a single valid block into a liveness failure. We share the first batch of findings.

Stefanos Chaliasos, Martín Ochoa, Varun Thakore · August 10, 2026

Circom-Auditor: Open-Source Skills for Finding Vulnerabilities in Circom Code

We are releasing zk-skills, a set of open-source security skills for AI coding agents, starting with circom-auditor: a first line of defense against vulnerabilities in Circom circuits, compatible with both Claude Code and Codex. On the zkbugs benchmark it detects up to 66 of 70 known bugs when pointed at the vulnerable circuits, and up to 40 of 56 when let loose on the full original codebases, far ahead of existing Circom security tools.

Stefanos Chaliasos, Hao Pham, False Witness Team · August 05, 2026
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

zk.golf: Fearless and Collaborative Optimization of Circuits

zk.golf is a platform where people can compete on creating the most efficient zk circuits for specific problems. It is enabled by what we call "fearless optimization", which is achieved by combining formal verification and frontier AI models. By the end, you will be convinced that nobody should look at constraints ever again in their life.

Giorgio Dell'Immagine, Mathias Hall-Andersen · July 02, 2026

The State of Security Tools for ZKPs

Zero-knowledge proofs (ZKPs) have come a long way from theory to real-world applications like blockchains and private transactions. We’ve been busy auditing various ZKP implementations and developing tools to improve circuit safety and security. In this blog post, we’ll explore how vulnerabilities can crop up in SNARK systems and the current state of tools designed to spot these issues. From circuit bugs to the often-overlooked frontend and backend layers, we cover how various analysis techniques and formal verification approaches are evolving to ensure robust ZKP systems. Dive in to discover the potential and current challenges in ZKP security!

ZK/SEC · June 02, 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