EthSystems Completes Formal Verification of Privacy Pool, Covering Sepolia Bytecode

Ethereum privacy technology organization EthSystems has announced the completion of formal verification for its privacy pool, covering the range from written specifications to bytecode on the Sepolia testnet. Various tools were used during the verification process, with models, circuits, and hashes utilizing Lean, contracts using Halmos and Kontrol, and wallets using Aeneas and Verus. The verifier and deployment were cross-checked through byte-by-byte reconstruction. Double-spending and value conservation have been verified by the Lean theorem prover. A total of 6 issues were identified during the verification, 3 of which were found in the verification tools themselves. The team also listed assumptions that still rely on, including hash collision resistance, the verifier rejecting forged proofs, and contract behavior being consistent with the model.

This content is provided for general informational purposes only and doesn't constitute financial, investment, legal, or tax advice. Any events, rewards, online promotions, or related information mentioned herein should not be considered a recommendation, solicitation, or invitation to purchase, sell, trade, or otherwise deal in any crypto assets. Crypto assets are highly volatile and may result in loss. The availability of WEEX services, products, and related events may vary by region. You are responsible for ensuring that your participation is in accordance with applicable local laws and regulations.