EthSystems has completed the formal verification of the privacy pool, covering the specifications to Sepolia bytecode

The Ethereum institutional privacy technology organization EthSystems announced the completion of formal verification for its privacy pool (shielded pool), ranging from written specifications to the bytecode running on the Sepolia test network. The verification used different tools in layers: models, circuits, and hashes with Lean; contracts with Halmos and Kontrol; wallets with Aeneas and Verus; and validators and deployment verified through byte-by-byte reconstruction.

Double spending and value conservation have been verified by the Lean theorem prover. During the verification, a total of 6 issues were discovered, 3 of which were found in the verification tools themselves. The team also listed the assumptions that still rely on: hash collision resistance, validators rejecting forged proofs, and contract behavior being consistent with the model.