What formal verification is
Formal verification proves, in machine-checked logic, that a system absolutely meets its specification. The proofs are written in a proof assistant, Lean 4, that checks every logical step: a property is either proven for all cases, or the build fails. While testing and audits sample behavior, formal verification covers every reachable state.
Privacy is where this becomes a requirement. Private state is encrypted onchain; you can see it’s there, not its content. The only way to know the rules are right is to prove them.
What is formally verified
First, three terms: a note is an encrypted balance (a sealed envelope of tokens); a nullifier is a one-time stamp that marks a note as spent so it cannot be reused; and registration is the one-time step that ties an account to its keys.
The privacy pool is modeled in Lean as a state machine: every action (register, open channel, open subchannel, create note, etc.) acting within the pool’s onchain state. Every property below is proven for every possible state reachable by any sequence of valid actions. The development runs to over 230 theorems, no unproven steps. The toolchain and its libraries are pinned, so anyone can rebuild the project and re-check every proof independently.
What the proofs establish:
- Notes cannot be forged. Creating a note requires a valid channel and subchannel; once written, notes, registrations, and nullifiers cannot be altered; and each note has exactly one owner, the intended recipient.
- No double-spend. Each note spends through a one-time nullifier, and no state-changing action can execute twice.
- Exact accounting. Value cannot be created or inflated: a note holds exactly what was created and deposited into it, and every spend is fully accounted for.
- Funds stay recoverable. Every note that exists is discoverable by its owner’s key scan, on both the incoming and outgoing side, and discoverability never regresses.
- Funds stay spendable. Any unspent note can always be spent, and a user can always spend down to a zero balance. There are no frozen-funds states.
- Permanent Compliance. With the compliance key, all notes are retrievable, and coin tracing works forward, the two directions are proven mutually inverse. Compliant disclosure is a proven capability of the protocol.
Beyond the pool
Verifying the pool is only part of the picture. The pool still relies on the layers beneath it: the compiler that builds the contract, and the Stwo-verifier that validates the proofs’ correctness. So we extended our formal verification work into those layers too.
Running a multi-year Lean-based verification program, in collaboration with Prof. Jeremy Avigad and Dr. Yoav Seginer, we have proved the correctness of the most delicate parts of the platform the pool runs on: the Stone and S-two provers’ encodings of Cairo execution, core CairoZero functions, and the Sierra-to-CASM compilation building blocks.
We formally verified the protocol. The Cairo contract that implements it is covered separately by the OpenZeppelin audit.
Our full formal verification development is now open source. The privacy pool’s proofs are available in the privacy SDK repository, allowing anyone to validate them. You can read more on our foundational work in our March 2026 write-up on formal verification.
