EthSystems Proves Two Shielded-Pool Guarantees in a Model, Leaves Privacy Claims Open

EthSystems has proved that its Ethereum shielded pool prevents double spending and preserves value in a formal model, while leaving privacy claims and key links to deployed contracts unproved.

A shielded pool lets users deposit tokens and receive private notes that they can transfer or withdraw using zero-knowledge proofs. A public nullifier marks a note as spent without identifying it. This design limits what transaction details are exposed publicly.

The verification work covered the system from its written rules through bytecode deployed on Sepolia. EthSystems used Lean for the model, circuits and hashes; Halmos and Kontrol for contract checks; and Aeneas and Verus on selected wallet functions.

Lean proved the two accounting guarantees in the model. The campaign also closed 20 of 36 contract obligations within its stated scope, including nine through contract checks. Separately, 12 deployed runtime codes matched an offline rebuild byte for byte.

That code comparison connects the deployed runtime codes to the rebuild, but does not establish who can change the contract later. The guarantees still depend on control of the contract’s owner key, as well as on the verifier rejecting false proofs and the contract behaving as the model specifies. They also assume hash collisions do not occur.

The verification applies to commit a04b8b3. The current code differs in the transfer circuit, verifier and pool contract, which remain outside the verification until the code pin is updated.

Confidentiality, unlinkability and selective disclosure were not proved for the deployed pool. Privacy was partially checked through conditional bounds in restricted models, but those results did not establish privacy for the deployed system.

The campaign identified six issues, three of them in verification tools. Two defects in Lampe, which translates Noir code into Lean, were fixed. A separate issue in evm-smith remained open. Updating the code pin is needed before the newer circuit and contracts fall within the verification’s scope.