The BN254 code in 25.2.0 shows both halves of the problem:

impl From<U256> for Fr {
    fn from(value: U256) -> Self {
        Self(value)
    }
}

impl PartialEq for Fr {
    fn eq(&self, other: &Self) -> bool {
        self.as_u256().partial_cmp(other.as_u256()) == Some(core::cmp::Ordering::Equal)
    }
}

So Fr::from_u256(r + 1) == Fr::from_u256(1) returned false. A contract that compares or stores numbers supplied by a caller could be told that two equal values differ. The type's documentation said that all arithmetic operations follow modulo r, which was true of the host arithmetic and untrue of the stored value.

Which soroban-sdk versions are affected?

Three release lines carried the bug.

Every release from 26.0.0 on carries the fix. Upgrading the SDK does not repair a contract that is already deployed. The SDK code is compiled into each contract, and the contract records the SDK version it was built with in its metadata. A contract built on a vulnerable release keeps the old behavior until it is rebuilt and upgraded or redeployed. None of the vulnerable releases has been yanked from crates.io, Rust's package registry, so a project can still install them.

What property catches the bug?

In plain words: when two numbers stand for the same value on the r-clock, the SDK's == must say they are equal, and when they stand for different values, it must say they differ. The rule takes two arbitrary 256-bit numbers and checks exactly that, comparing == on the SDK type against equality mod r:

/// P1 on BN254, through Fr::from_u256.
#[rule]
pub fn bn254_fr_eq_iff_same_element(e: Env) {
    let r = modulus(&e, &BN254_R_BE);
    let u = any_u256(&e);
    let v = any_u256(&e);

    let same_element = u.rem_euclid(&r) == v.rem_euclid(&r);
    let fr_equal = bn254::Fr::from_u256(u) == bn254::Fr::from_u256(v);

    cvlr_assert!(fr_equal == same_element);
}

any_u256 returns an arbitrary 256-bit number, so the Certora Prover considers every possible pair. A unit test checks the inputs someone thought to try. This is the gap between testing and formal verification.

Each curve has three rules. The one above compares two values. A second checks the stored value directly: building an Fr from u should store u mod r. A third asks the Prover to find two different numbers that are the same field element. That third rule guards against a vacuous result, where a property passes or fails because the case it describes can never occur, a failure mode covered in How Formally Verified Code Goes Wrong and How to Catch It.

What does the Prover report on 25.0.0 and 25.2.0?

On both releases, the equality rule and the stored-value rule fail on both curves, and the third rule finds the pair of numbers it asks for (Prover reports: 25.0.0, 25.2.0). In the BN254 counterexample for the equality rule, the two numbers are:

u = 0xe260000000000000000000000000000000000000000000000000000000000001
v = 0x20cec6347b397f591ebee925f9fa9e8b5f305ede191a3dbaf07829b03ffffffd

They differ by exactly four times r, so they are the same field element, and Fr::from_u256(u) == Fr::from_u256(v) returned false. The BLS12-381 counterexample has the same shape, with u = v + r. In the BN254 counterexample for the stored-value rule, u lies between r and 2r and is stored without being reduced.

The Prover did not discover this bug. The rule was written after the advisory and against it, so the failures confirm the behavior the advisory describes. What the rule adds is a property a developer can write once and run on every release. It fails on 25.0.0, the first stable release with BN254, as well as on 25.2.0, so it catches the bug on the first and the last vulnerable 25.x release, not only the last.

What does the bug allow in a privacy pool?

A privacy pool lets a user withdraw a deposit without revealing which deposit was theirs. Each withdrawal publishes a nullifier, a number derived from the deposit, and the pool records it so the same deposit cannot be withdrawn twice.

Stellar's privacy-pools example reads each public input of a withdrawal proof with Fr::from_u256 and records spent nullifiers by their raw bytes. Its proof check reduces each input mod r on the host. On a vulnerable SDK, that accepts a proof with nullifier n and then the same proof with n + r. The proof check treats both as n, while the recorded bytes of n and n + r differ.

A local test confirmed it. Using the example's own valid proof on soroban-sdk 25.1.0, the first withdrawal succeeded, and the same proof with the nullifier replaced by n + r paid out a second time. On soroban-sdk 27.0.0, the second withdrawal was refused with "Nullifier already used." The test ran locally and touched no deployed contract. The example is a reference for developers, and nothing shows it deployed on mainnet.

The pattern is older than Soroban. In 2019, Semaphore issue #16 reported that Semaphore.sol did not check that a nullifier was below the field modulus, so the nullifier hash plus the modulus would also pass verification and allow a double spend. One layer treats n and n + r as the same value and another treats them as different.

How can you run the rules yourself?

Certora has published the rules, the unit tests and the privacy-pool test in a public gist. You need Rust with the wasm32v1-none target, Python 3, Java 21, certora-cli and a Certora key. Copy the files into src/ and confs/, run cargo test for the four unit tests, which all fail on 25.2.0, then run certoraSorobanProver fr.conf from confs/. The README explains how to switch the SDK to another release to compare results.

This rule is one small piece of Certora's Stellar work. The team verified Blend V1 at the Wasm bytecode level with the Sunbeam Prover and reviewed the Stellar and Rust version of Huma Protocol. The Stellar Security Hub collects the Sunbeam docs, a demo video and a workshop video for getting started.

What can the Prover show here, and what can it not?

The rules cover how soroban-sdk builds an Fr from a 256-bit number and compares two of them, on both curves, on 25.0.0 and 25.2.0. The Prover reasons about Soroban through Certora's model of the host functions the rules call, and a proof holds within its model.

That model limits what the Prover can say about the fix. The fix relies on deciding which of two large numbers is bigger, and the Prover's Soroban model cannot yet do that, so the fixed release 25.3.0 does not get a clean verdict. The four unit tests, which run the Soroban host's own code, all pass on 25.3.0. The rules also say nothing about values a contract keeps as plain integers or raw bytes without ever turning them into an Fr, contracts already deployed with a vulnerable SDK, the SDK's other cryptographic types, or the soundness of any circuit or verifier.

How did soroban-sdk 25.3.0 fix the bug?

The SDK now reduces every number mod r at the moment an Fr is built. Every stored value is below r, so two stored values are equal exactly when they are the same field element. PR #1750 leaves == untouched. The conversion from a 256-bit integer reduces any value at or above r, and every other way of creating an Fr, contract arguments included, goes through it. The same release also made the base-field types Fp and Fp2 reject out-of-range values, which the advisory lists as a separate hardening.

What should teams do about CVE-2026-32322?

A contract built on 22.0.0 to 22.0.10, 23.0.0 to 23.5.2 or 25.0.0 to 25.2.x that compares or stores caller-supplied scalars needs a rebuild on a fixed release and a contract upgrade. The contract's metadata records which release it was built with. If the move to a fixed release has to wait, the advisory's workaround is to reduce the U256 by r with rem_euclid before constructing an Fr. That is also a code change, so the contract still has to be upgraded or redeployed. For BN254 it is the only option, because BN254 had no Fr host functions before Protocol 26.

A contract that keeps scalars as U256 values or as bytes, as nullifier keys or in events, needs its own check on any SDK version: reject every value at or above r where the input enters the contract. The SDK fix reduces a value once it becomes an Fr and does nothing for a copy kept in another type.

Key takeaways from CVE-2026-32322

The bug sat between two layers that disagreed about what a scalar is. The host reduced every scalar mod r and the SDK type stored it as given, so each layer was consistent with itself and the contract on top inherited the disagreement. Any library that hands a value to arithmetic in one representation and compares it in another has the same gap.

The property that catches it fits in one sentence: equality on the type agrees with equality of the values it represents. A short rule stating that sentence fails on the first stable release with BN254, and it can run on every release a library ships.
--

Follow Certora on X and LinkedIn.

Try the Sunbeam Prover on your own Soroban code.

See how AutoProver now supports Rust code.

Request a Certora audit, combining manual review with formal methods.