Soroban SDK 25.0.0-25.2.x contained a field arithmetic bug where equal cryptographic values compared as different. This affected zero-knowledge proof comparisons in contracts like privacy pools, potentially allowing double-spends. Certora's Sunbeam Prover caught it with a one-line formal verification rule that no unit test had written.
Soroban SDK 25.0.0-25.2.x stored field arithmetic values without reducing them modulo r, the prime modulus of elliptic-curve arithmetic. This caused two mathematically equal values (e.g., n and n+r) to compare as different when using the Fr type for BN254 and BLS12-381 curves. In privacy pools, this allowed the same zero-knowledge proof to succeed twice: the host reduced inputs mod r before checking the proof, but the contract's spent-nullifier list stored unreduced values, so n and n+r were treated as different. Certora's Sunbeam Prover caught the bug by writing a formal verification rule: if two 256-bit numbers represent the same field element, their equality check must return true. The rule failed on all vulnerable releases and passes on the fixed SDK 25.3.0+. No public exploitation was reported.
