EthSystems hoàn tất xác minh hình thức của Privacy Pool

The Huoxing Finance report states that EthSystems, an institutional privacy technology organization for Ethereum, has announced the completion of formal verification for its shielded pool, covering everything from written specifications to the bytecode running on the Sepolia testnet. Different tools were used at each layer: Lean for models, circuits, and hashes; Halmos and Kontrol for contracts; Aeneas and Verus for wallets; and verification and deployment were cross-checked through byte-by-byte reconstruction. Double-spending and value conservation have been verified by the Lean theorem prover. Six issues were identified during verification, three of which were in the verification tools themselves. The team also listed remaining assumptions: hash collision resistance, validators rejecting forged proofs, and contract behavior matching the model.