Unfaithful claims: breaking 6 zkVMs

A zkVM verifier should be faithful to its public claims. If a statement about a program’s inputs or outputs is false, verification must fail.

We found six systems where this guarantee breaks. In Jolt, Nexus, Cairo-M, Ceno, Expander, and Binius64, values that affect verification weren’t always bound to the Fiat-Shamir transcript before challenges were generated. This lets an attacker choose those values after seeing the challenges and solve for whatever makes the verifier accept.

The resulting proofs can convince a verifier of mathematically impossible statements, such as a counterexample to Fermat’s Last Theorem. In a blockchain context, this could translate to receiving $1M out of thin air. We’ve included two challenges at the end of this post if you’d like to try implementing the exploits yourself.

What are we even breaking?

A zkVM proof claims that a program executed correctly on public inputs and produced the claimed public output, without revealing the full execution trace. We can write this as a claim that a valid trace $T$ exists.

Here, $P$ is the public program or circuit description, $X$ is its public input, and $Y$ is the claimed public output. The private trace $T$ contains the registers, memory history, and intermediate values from execution.

The verifier doesn’t replay that execution. It checks algebraic constraints over committed polynomials. A polynomial commitment binds the prover to a polynomial and lets them later prove an evaluation, such as “my polynomial evaluates to 42 at point 7,” without revealing the whole polynomial. We’ll refer to the polynomial commitment scheme as the PCS.

Some systems in this post provide verifiable computation without full zero knowledge. The property we’re breaking in all six is soundness, which requires that false execution claims don’t verify. This is distinct from completeness, which requires that honest executions do verify.

All six verifiers follow roughly the same process. They start with a public statement and metadata such as sizes, roots, and domains. They read commitments, reduction messages, and claimed evaluations from the proof, reconstruct the Fiat-Shamir challenges, and check the constraint equations at the sampled points. Opening proofs connect those evaluations to the polynomial commitments, and the verifier accepts only if the constraint, opening, and global consistency checks agree.

The ordering of these operations matters. If a value affects a verification equation but isn’t bound before the relevant challenge is sampled, the prover may be able to choose it after learning what the verifier will check.

The building blocks

To see why this is exploitable, let’s work through the protocols involved.

The Fiat-Shamir transform

In an interactive protocol (the type most commonly described in literature), the verifier sends random challenges and the prover responds in real time. That doesn’t work well for blockchains, where there is no live verifier, or for proofs that anyone should be able to verify later.

The Fiat-Shamir transform replaces the verifier’s randomness with a cryptographic hash function. Both parties maintain a transcript, which is the running hash state of the protocol. Adding data to that state is called absorbing it, and deriving a challenge is called squeezing.

After absorbing the public statement, the prover can derive challenges from their own transcript and respond to them without contacting a verifier. The verifier starts with the same statement and replays the same operations to recover the challenges.

The hash makes the challenges unpredictable before the relevant values are fixed. But if some value $V$ hasn’t been absorbed when a challenge is squeezed, that challenge is independent of $V$. The prover can compute the challenge first, then choose $V$ to make the verification equation pass. That is the bug class we found in all six systems.

The sumcheck protocol

The sumcheck protocol proves that a polynomial sums to a claimed value over the Boolean hypercube, meaning all inputs in $\{0,1\}^n$. The claimed sum is

Computing this directly would require the verifier to evaluate all $2^n$ terms. Sumcheck reduces that work to checking one evaluation of the original polynomial, after a sequence of rounds.

In each round, the prover sends a polynomial $g_i(X)$ such that $g_i(0) + g_i(1)$ equals the previous claim. If the original sum $H$ is false, the prover must lie about one of these polynomials. Since the verifier picks a random $r_i$ after receiving $g_i$, the lie won’t match the evaluation of the original polynomial except with very low probability.

There is also a communication optimization that will matter for the attacks. A degree-1 polynomial $g_i(X) = a + bX$ has only two coefficients. Since the verifier already knows the previous claim $H_{i-1}$, they can recover $b$ from $a$.

The prover only needs to send $a = g_i(0)$, saving 50% of the communication for these coefficients. Substituting the recovered value of $b$ into the next claim gives us

Notice that this is linear in $H_{i-1}$. Applying the same reasoning through all rounds, the final claim is linear in the original $H$. If $H$ isn’t in the transcript, we can hold the challenges fixed and solve for the value of $H$ that the verifier will accept.

Multilinear extensions

A multilinear extension (MLE) turns a table of values over $\{0,1\}^n$ into a polynomial. It agrees with the table at Boolean inputs and interpolates between them at other field points.

The property we’ll use is that evaluating an MLE at a fixed point is linear in the table entries.

At a fixed challenge point $\vec{r}$, the coefficients $\text{eq}(\vec{b}, \vec{r})$ are constants. An attacker who can change the table values after $\vec{r}$ is known can therefore solve for alternative values that preserve the same evaluation.

Lookup arguments

A zkVM needs to check properties such as whether a byte is in $[0, 255]$, an opcode decodes correctly, or a memory access agrees with earlier accesses. Adding separate constraints for every check is expensive. Lookup arguments let the system precompute a table of valid tuples and prove that the values used during execution belong to it.

LogUp, a lookup argument based on logarithmic derivatives, expresses multiset relations as sums of fractions. For two multisets $A$ and $B$ that should be equal, it checks

at a random challenge $z$. Matching multisets give equal sums. Different multisets give different sums with overwhelming probability.

In a zkVM, components produce and consume lookup tuples. The CPU might emit a record saying it read value $v$ from address $a$ at time $t$, while the memory table consumes the corresponding record. Each component’s claimed_sum is its net contribution to the LogUp sum.

The global check requires $\sum_i \text{claimed}\_\text{sum}_i = 0$, so everything produced must be consumed. However, the claimed_sum values come from the prover. If they aren’t bound before the relevant challenges are derived, the prover can adjust them to make an invalid execution balance.

Solving for an unbound claim

The attacks start by finding a value the prover controls and checking when it enters the transcript. We then trace that value through the verifier to find every equation it affects. With the transcript and challenges held fixed, the unbound values become the unknowns in a system of equations.

For a single value $V$, the check has the form $f(V) = \text{target}$. If $f$ is linear, solving it requires only field arithmetic.

This doesn’t require breaking the commitment scheme. We solve for a value that satisfies the existing check and put it into the proof or public statement.

When several unbound values affect several checks, we have to satisfy them together. Gaussian elimination solves a linear system in $O(n^3)$ field operations. Some of the systems below introduce nonlinear constraints, which may require techniques such as resultants or Groebner bases.

The six broken systems

Jolt, Nexus, and Ceno leave intermediate claims in the proof unbound. Cairo-M, Expander, and Binius64 have the same problem with public statement data. Let’s start with Jolt to see how the sumcheck optimization turns into an exploit, then work through the differences in the other systems.

Jolt (a16z)

Jolt is a zkVM for RISC-V programs, built by a16z. It uses sumcheck extensively to verify execution constraints, with commitments, opening claims, and the corresponding proofs stored in JoltProof.

JoltProof {
    commitments: Vec<Commitment>,           // Polynomial commitments to trace
    opening_claims: Map<OpeningId, Claim>,  // <- THE VULNERABLE VALUES
    proofs: Map<Stage, SumcheckProof>,      // Sumcheck and opening proofs
    ...
}

The verifier first initializes the transcript and absorbs the public inputs and outputs, trace length, and commitments. Stages 2–4 derive batching coefficients and verify the batched sumchecks. Stage 5 verifies the polynomial evaluations against the commitments.

Each sumcheck instance provides an input_claim, the value that its polynomial allegedly sums to over the Boolean hypercube. These values come from opening_claims, but they were never absorbed into the transcript before the batching coefficients were derived.

The verifier computes BatchedClaim as a random linear combination of the individual claims $H_i$.

The coefficients $\alpha_i$ come from the transcript. Since the $H_i$ values weren’t in that transcript, the coefficients are independent of the claims they’re meant to check.

Recall the sumcheck compression optimization. The prover omits one coefficient per round, and the verifier reconstructs it using the previous claim. Following this through the rounds makes the final verification equation linear in the input claim $H$.

Here, $a$ and $b$ are determined by the transcript and are independent of $H$. The verifier compares $C_{\text{final}}$ with $\text{expected}\_\text{eval}$ from the PCS opening, giving us $a \cdot H + b = \text{expected}\_\text{eval}$.

Multiple claims are coupled across verification stages, so changing one claim may affect several checks. We can account for all of them by solving a small linear system over a handful of unbound claim values.

Jolt fixed the issue on October 3, 2025 in PR #981.

Nexus

Nexus is a zkVM built on StarkWare’s Stwo prover. It divides verification into components for instruction execution, memory, registers, and other parts of the machine. Each component handles a subset of the execution constraints.

These constraints are polynomial equations describing a valid execution trace, an algebraic intermediate representation (AIR). Nexus uses STARKs to check them with commitments, random sampling, and a low-degree test called FRI. FRI stands for “Fast Reed-Solomon IOP” and checks that a committed function is a low-degree polynomial. This approach doesn’t require a trusted setup.

Like the lookup example above, each Nexus component produces and consumes tuples. Its claimed_sum records the net contribution.

The claimed sums must add to zero so that every produced tuple is consumed. They are included alongside the STARK proof and component sizes in NexusProof.

NexusProof {
    stark_proof: {
        commitments: [Merkle roots of trace columns]
        sampled_values: [polynomial evaluations]
        fri_proof: [low-degree test proof]
    }
    claimed_sum: [FieldElement; NUM_COMPONENTS]  // <- VULNERABLE
    log_size: [component sizes]
}

The verifier derives lookup elements, an out-of-domain point, and composition coefficients from a transcript containing associated_data, log_sizes, and trace commitments. It checks that the claimed_sum array has the correct length and sums to zero, but never absorbs those values into the transcript.

The verifier combines the execution constraints into a composition polynomial.

The verifier checks this polynomial at a random point outside the execution domain. This is the out-of-domain sampling (OODS) test, which requires $C(\text{oods}\_\text{point}) = \text{expected}$.

The LogUp boundary constraints are linear in the claimed sums. Once the challenges are fixed, their contribution to the composition polynomial is linear as well. We therefore need to satisfy both the OODS check and the requirement that the claimed sums add to zero. Together, these form a small linear system.

Nexus fixed the issue on October 24, 2025 in PR #503.

Cairo-M (Kakarot Labs)

Cairo-M, built by Kakarot Labs, is an alternative proof system for the Cairo VM used by Starknet. Like Nexus, it uses LogUp to prove global statements about execution. The unbound values in this case are the public inputs and outputs, boundary registers, clock, and memory roots in public_data.

Proof {
    claim: ComponentSizes,
    interaction_claim: LogupClaimsPerComponent,
    public_data: {          // <- VULNERABLE
        initial_registers: { pc, fp },
        final_registers: { pc, fp }, // <- forged
        clock,                       // <- forged
        initial_root,
        final_root,                  // <- forged
        public_memory: { program, input, output }, //output modified
    },
    stark_proof: [...],
}

The verifier processes the PCS configuration, trace roots, component sizes, and proof-of-work check before drawing the lookup challenges $z$ and $\alpha$. At this point, public_data hasn’t been mixed into the transcript. It is then used in the global lookup check, after which the verifier mixes interaction_claim and verifies the STARK proof.

The public data enters the lookup relations through challenge-weighted encodings of tuples in the denominators. Abstractly, the verifier checks

With the challenges fixed, this is a rational equation in the public data. We can still solve it algebraically, but the linear approach from Jolt and Nexus isn’t enough.

The public data participates in verification through extension-field arithmetic, including public-memory entries that take values in the extension field. Finding forged parameters therefore requires solving a coupled system over that extension field.

Cairo-M fixed the issue on October 31, 2025 in commit 92b6740.

Ceno (Scroll)

Ceno is a zkVM by Scroll that uses GKR, a protocol that verifies arithmetic circuits layer by layer with sumcheck. This reduces verification of a large circuit to a few random evaluations.

Ceno divides verification into chips, one per opcode or lookup table. Each chip proves its constraints independently. Values associated with reads, writes, and lookups are batched into a binary tree, whose layers fold pairs of values using random challenges. This is the tower sumcheck.

Read records must match write records after accounting for the initial and final state. Ceno checks this multiset equality with a product rather than a LogUp sum.

The evaluations used in these checks are included in ZKVMChipProof.

ZKVMChipProof {
    r_out_evals: [[FieldElement]],   // <- VULNERABLE
    w_out_evals: [[FieldElement]],   // <- VULNERABLE
    lk_out_evals: [[FieldElement]],  // <- VULNERABLE
    tower_proof: [...],
    gkr_iop_proof: [...],
}

The r_out_evals, w_out_evals, and lk_out_evals values initialize the tower sumcheck claim, but they are never absorbed into the transcript. The tower claim is $\text{claim} = \sum_j \alpha^j \cdot \text{out}\_\text{evals}_j$, which is linear in those evaluations.

We also have to satisfy the product check. If we vary $x_0 = {\text{r}\_\text{out}\_\text{evals}}[0][0]$ and $x_1 = {\text{r}\_\text{out}\_\text{evals}}[0][1]$ while fixing the other evaluations, the constraint becomes

This is bilinear in $(x_0, x_1)$. Together with the linear GKR equation, we have two equations in two unknowns.

Substituting the linear equation into the product equation reduces the system to a quadratic in one variable, which we can solve with the quadratic formula.

Ceno fixed the issue on March 5, 2026 in PR #1262. The original report is available in issue #1125.

Expander (Polyhedra)

Expander is a GKR-based proof system for arithmetic circuits. Its proof bytes contain a PCS commitment, sumcheck round polynomials for each layer, layer claims claim_x and claim_y, and PCS opening proofs, in that order. The statement values public_input and claimed_v are passed separately.

In Expander’s circuit model, constant gates can reference public input values. During GKR verification, eval_cst() computes their contribution at the sumcheck challenge point.

sum -= GKRVerifierHelper::eval_cst(&layer.const_, public_input, sp);

The coefficients come from challenges stored in the verifier’s scratch pad, sp. The evaluation is a linear combination of the public inputs.

However, the transcript is built from proof bytes, including the PCS commitment and sumcheck round messages. The separately supplied public_input and claimed_v values are never absorbed.

The challenge vector $\vec{r}$ is therefore independent of public_input. We can choose a false statement, such as a forged output, and solve the resulting linear constraints for a modified public input that makes the verifier accept.

Expander fixed the issue on January 21, 2026 in commit 4a8c2be. The claimed 500k bug bounty award is pending.

Binius64

Binius64 is a proof system designed for 64-bit CPUs that operates over binary fields such as $\mathbb{F}_{2^{128}}$, where addition is XOR. Its shift protocol handles bit shifts and rotations, operations used by hash functions such as SHA-256.

The verifier receives the public witness, containing program inputs and outputs, as a separate parameter.

pub fn verify<F, C>(
    constraint_system: &ConstraintSystem,
    public: &[Word],    // <- NEVER ABSORBED
    // ...
) -> Result<VerifyOutput<F>, Error>

The first sumcheck produces $\gamma$ and challenge points r_j for bit indices and r_s for shift indices. The verifier then samples inout_eval_point and batch_coeff from the transcript. The public witness hasn’t been bound before these challenges are sampled.

Using the unbound public slice, the verifier computes public_eval = MLE(public, r_j, inout_eval_point). This evaluation is linear in the public witness bits.

The result feeds a second sumcheck through the batched sum $\gamma + \text{batch}\_\text{coeff} \cdot \text{public}\_\text{eval}$.

Because the challenges are independent of public, an attacker can look for an alternative witness $\text{public}'$ with the same evaluation. This gives one 128-bit linear constraint over hundreds of witness bits. Under common parameterizations, the system is underconstrained and admits many alternative witnesses, allowing a different public statement to pass the same check.

Binius64 fixed the issue on December 29, 2025 in commit 86a515f.

Why does this keep happening?

Finding the same bug in six independent implementations makes it hard to treat these as isolated mistakes. We found them by examining only a handful of systems, while dozens of zkVMs, proof systems, and recursive verifiers are deployed today.

Academic papers usually describe interactive protocols, where the prover sends a commitment $C$, the verifier responds with a random challenge $r$, and the prover sends a response $R$. Security proofs analyze that interaction, where the ordering is implicit. Papers often leave out the steps needed to make it non-interactive, including hashing $C$, the public statement, and any intermediate values before deriving the challenges that depend on them. The implementer has to work out those bindings, which requires understanding the full protocol.

Modularity makes this harder. A zkVM layer may pass a claim to a lookup layer, which passes it to a sumcheck layer. Each can assume that another layer has already bound the value. If none of them does, an unbound claim reaches the verifier.

There is also pressure to avoid unnecessary hashing. Every hash has a cost, and some values can safely be omitted from the transcript. Deciding which ones can be left out requires understanding all the protocols involved and having that reasoning checked by experts.

Ordinary testing is unlikely to find the attacks we’ve described. Unit and integration tests generally run an honest prover, while random fuzzing is very unlikely to stumble onto the values that satisfy the verifier’s equations for a false statement. Finding these bugs requires manual security analysis, and even that can miss them.

Preventing missing bindings

The fixes in these six cases were only one or two lines of code. Finding them required understanding the full verification flow. For an audit, we need to map that flow and check each prover-controlled value against the point where its relevant challenges are derived. The question to ask is, “What if the prover chose this value after seeing the challenges?”

One way to make missing bindings less likely is to merge the proof buffer and transcript. The buffer emulates the communication channel between prover and verifier. Whenever the prover writes a value, that value is automatically absorbed. When the prover needs a challenge, it is squeezed from the current transcript.

The verifier reads the same buffer in the same order, absorbing values as it goes and reproducing the challenges. Halo2 follows this pattern, and Binius also organizes its proof handling around the transcript.

With dozens of components, each with its own inputs and outputs, “hash everything” is difficult to turn into a precise implementation rule. The responsibility for each binding needs to be explicit. If there is doubt about whether a value can safely be omitted, absorb it.

Responsible disclosure timeline

We notified all six teams. Responses ranged from immediate acknowledgement to delayed fixes, and all reported issues have since been addressed.

Challenges

We’ve prepared two challenges if you’d like to practice implementing these exploits. If you solve either one, follow the instructions in the flag. The first 10 solvers will get a T-shirt.

Your goal is to convince the verifier that you know a counterexample to Fermat’s Last Theorem. Find $a, b, c \ge 1$ such that $a^3 + b^3 = c^3$. Good luck!

The Jolt handout contains the setup running on the server. Submit your proof by connecting to jolt.chal.osec.io:8960.

The Nexus handout contains the setup running on the server. Submit your proof by connecting to nexus.chal.osec.io:8950.

Now you should have enough margin to prove Fermat wrong.