PANews reports on May 14th that according to the Ethereum Foundation website, blockchain security institution CertiK has recently been awarded two research grants from the Ethereum Foundation for the first quarter of 2025, focusing on developer tools and improvements in zkVM circuit verification methods:
Verus Tool Assessment: CertiK will evaluate the utility of Verus (a Rust verification tool) in verifying circuits written in Rust and EVM pre-compiled modules.
zkVM Circuit Verification Simplification: The project aims to develop strategies to simplify zkVM circuit verification, with a focus on addressing module arithmetic and packing multiple numerical values into a single domain element.
It is understood that CertiK's formal verification technology has been widely applied in multiple top Web3 projects such as zkWasm, TON main chain contracts, Cosmos SDK, Ant Group's HyperEnclave TEE, and Asterinas OS.
