EthSystems, an Ethereum institutional privacy technology organization, announced the completion of formal verification for its shielded pool, covering the full stack from written specification to bytecode deployed on the Sepolia testnet. The verification employed specialized tools at each layer: Lean for the model, circuits, and hashing; Halmos and Kontrol for smart contracts; Aeneas and Verus for the wallet; and byte-by-byte reconstruction checks for the verifier and deployment. Double-spending and value conservation properties were machine-verified through Lean theorems. Six issues were identified during the process, three of which stemmed from the verification tools themselves. EthSystems noted remaining assumptions including hash collision resistance, verifier rejection of forged proofs, and contract consistency with the formal model.