EthSystems Completes Formal Verification of Privacy Pool, Covering Spec Through Sepolia Bytecode

October 27: EthSystems, an Ethereum institutional privacy technology organization, announced that it has completed formal verification of its shielded pool, covering everything from the written specification to the bytecode running on the Sepolia testnet. The verification used different tools at each layer: Lean for the model, circuits and hashing; Halmos and Kontrol for the contracts; Aeneas and Verus for the wallet; and byte-by-byte reconstruction checks for the verifier and deployment. Double-spending and value conservation were machine-verified by Lean theorems. A total of 6 issues were found during verification, 3 of which were in the verification tools themselves. The team also listed the assumptions it still relies on: hash collision resistance, that the verifier will reject forged proofs, and that the contracts behave consistently with the model.