CertiK Completes Second Ethereum Foundation Grant on Formal Verification in zkVMs Using Verus
CertiK has finalized its second Ethereum Foundation grant, experimenting with formal verification of zkVM circuit correctness proofs using the Verus proof assistant. The work builds on a previous grant that developed open-source Rocq tactics for similar projects.
Last week @CertiK delivered and finalized their 2nd Ethereum Foundation grant relating to formal verification in zkVMs. This time the CertiK FV team experimented with zkVM circuit correctness proofs in Verus! More below 👇
In a previous grant (https://github.com/CertiKProject/rocq_zkvm_tactics) for the Ethereum Foundation, we developed an open-source set of automated tactics for Rocq, which aim to make similar future projects easier.
In this current work (github.com/CertiKProject/…) as an experiment we re-implemented part of the old zkWasm proofs using a different proof assistant, Verus, instead of Rocq. Verus is integrated with a powerful automatic (SMT) theorem prover, and the goal of this work was to see how helpful that woul
If you have any comments or questions about CertiK’s work in the FV space or if you would like to hear about our FV services please DM me 🙂