PANews reported on May 14 that, according to the official website of the Ethereum Foundation, the blockchain security agency CertiK recently received two research grants from the Ethereum Foundation for the first quarter of 2025, focusing on enhancing developer tools and formal methods for zkVM circuit verification.
Verus Tool Evaluation: CertiK will evaluate the practicality of Verus (a Rust verification tool) in 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 addressing modular arithmetic and the case of packing multiple values into a single field element.
It is reported that CertiK's formal verification technology has been widely applied in several top Web3 projects such as zkWasm, TON mainchain contracts, Cosmos SDK, as well as Ant Group's HyperEnclave TEE, Asterinas OS, and others.
