CertiK Says Coq Proofs Show zkWasm's Core Circuits Are Sound
- —Coq proofs establish soundness and knowledge soundness of zkWasm's circuits
- —The internal development spans about 33,000 lines of Coq, roughly 21,000 of them proofs
- —Two bugs were found: a missing memory-load constraint and missing Return constraints
- —Out of scope: Rust table-generation code, the Wasmi interpreter and Halo2 itself
Why it matters: Formal verification of zkVMs reduces the risk of forged proofs that underpin ZK bridges and L2 security.
Source: BlockchainReporter