[EthSystems Completes Formal Verification of its Shielded Pool, Covering Specification to Sepolia Bytecode] EthSystems, the Ethereum privacy technology organization, announced the completion of formal verification of its shielded pool, covering everything from the written specification to the bytecode running on the Sepolia testnet. Verification used different tools layer by layer: Lean for the model, circuits, and hashes; Halmos and Kontrol for contracts; Aeneas and Verus for wallets; and validators and deployments were verified through byte-by-byte reconstruction. Double-spending and value conservation were verified using Lean's theorem machine. Six issues were identified during the verification, three of which were related to the verification tools themselves. The team also listed the assumptions that remain: hash collision-free, validators rejecting forged proofs, and contract behavior consistent with the model.