According to the official website of the Ethereum Foundation, blockchain security firm CertiK has recently been awarded two research grants for the first quarter of 2025 by the Ethereum Foundation, focusing on enhancing formal methods for developer tools and zkVM circuit verification:

  1. Verus Tool Evaluation: CertiK will assess the practicality of Verus (a Rust verification tool) in verifying circuits written in Rust and EVM precompiled modules.

  2. Simplification of zkVM Circuit Verification: This project aims to develop strategies to simplify zkVM circuit verification, with a focus on addressing the arithmetic of modules and the packaging of multiple values into a single field element.

It is reported that CertiK's formal verification technology has been widely applied in top Web3 projects such as zkWasm, TON main chain contracts, Cosmos SDK, as well as Ant Group's HyperEnclave TEE, Asterinas OS, and others.