PANews reported on May 14 that according to the official website of the Ethereum Foundation, blockchain security agency CertiK recently won two research grants from the Ethereum Foundation in the first quarter of 2025, focusing on developer tools and formal means of zkVM circuit verification:
Verus Tool Evaluation: CertiK will evaluate the usefulness of Verus, a Rust verification tool, for verifying circuits written in Rust and EVM precompiled modules.
zkVM Circuit Verification Simplification: This project aims to develop strategies to simplify zkVM circuit verification, focusing on modular arithmetic and cases where multiple values are packed into a single domain element.
It is reported that CertiK's formal verification technology has been widely used in zkWasm, TON main chain contracts, Cosmos SDK, as well as Ant Group's HyperEnclave TEE, Asterinas OS and many other top Web3 projects.
