When Privacy Needs a Proof: Starknet’s STRK20 Formal-Verification Push

Privacy systems create a difficult verification problem: the ledger hides transaction details precisely when developers need confidence that the rules are correct. StarkWare’s latest STRK20 release addresses that problem with a machine-checked model of its privacy pool, published on July 23, 2026.

The central idea is to treat the pool as a state machine. In STRK20, encrypted balances are represented as notes, while nullifiers prevent the same note from being spent twice. The Lean 4 development models actions such as registration, channel creation, subchannel creation, and note creation, then proves properties across every state reachable through valid action sequences.

StarkWare says the project contains more than 230 theorems with no unproven steps, and that its pinned toolchain allows developers to rebuild and re-check the proofs. The claimed guarantees are practical rather than cosmetic: notes cannot be forged, nullifiers prevent double-spending, value cannot be inflated, owners can discover their notes, and unspent notes remain spendable. The model also covers a compliance path in which a compliance key can retrieve notes and trace coins forward.

That matters because STRK20 is designed as infrastructure for private assets rather than as an isolated mixer. Starknet’s builder announcement describes an open Privacy SDK and Wallet API. The SDK exposes low-level control over viewing keys, notes, proving, and on-chain submission; the Wallet API lets ordinary applications request shield, transfer, unshield, or swap operations through a privacy-enabled wallet. Each private transaction carries a ZK-STARK proof that notes are valid and unspent and that value is conserved, while sender, receiver, and amount remain hidden inside the pool.

The new verification layer changes what builders should inspect. A team integrating a private wallet or DeFi flow should not stop at checking whether a proof verifies. It should ask what the proof system is proving about the state machine, whether note discovery remains complete after every transition, how nullifiers are scoped, and what information a viewing or compliance key can reveal. Those questions turn privacy from a front-end feature into an auditable protocol boundary.

There is an important limitation. The formal-verification claims in this article come from StarkWare’s first-party announcement and should be independently rebuilt before being treated as an external audit result. The published proofs cover the modeled protocol and selected underlying components; StarkWare says the deployed Cairo contract is covered separately by an OpenZeppelin audit. Formal verification therefore strengthens confidence in specified properties, but it does not automatically certify every implementation, integration, key-management process, or operational assumption.

For ZK developers, the larger lesson is that privacy needs two proofs: a cryptographic proof that a transaction follows the rules without revealing its private data, and a formal proof that the rules themselves preserve the assets and guarantees the application promises. STRK20’s open Lean development is a concrete move toward making both layers inspectable.