Loading...
EthSystems completed the formal verification of the shielded pool, ranging from the written specification to the Sepolia testnet bytecode. The verification process utilized tools such as Lean, Halmos, Kontrol, Aeneas, and Verus, and involved a byte-by-byte reconstruction and verification of the validators and deployments. Double-spending and value conservation were machine-verified using Lean's theorem. Six issues were identified during the verification, three of which stemmed from the verification tools. The team listed the remaining dependency assumptions, including hash collision-free operation, validators rejecting forged proofs, and contract behavior consistent with the model.