This story was originally published on HackerNoon at:
https://hackernoon.com/certik-completes-formal-verification-of-zkwasm-mathematically-proving-the-zkvm-sound.
CertiK used the Coq proof assistant to prove zkWasm's circuits sound across its full instruction set, catching a design bug audits missed.
Check more stories related to programming at:
https://hackernoon.com/c/programming.
You can also check exclusive content about
#certik,
#web3,
#ai-and-ml,
#cybersecurity,
#software-engineering,
#technology,
#good-company,
#zkevm, and more.
This story was written by:
@ishanpandey. Learn more about this writer by checking
@ishanpandey's about page,
and for more stories, please visit
hackernoon.com.
CertiK has completed a formal verification of zkWasm, the zero-knowledge virtual machine for WebAssembly built by Delphinus Lab. Using the Coq proof assistant, it proved the zkVM's Halo2 circuits sound and knowledge sound across arithmetic, bitwise, memory, control-flow and function-call instructions. The work, which CertiK began in 2024, runs to more than 33,000 lines of machine-checked Coq and caught a critical design bug that auditing had missed. It arrives as Ethereum prepares to verify its own blocks with zkVM proofs, with the Ethereum Foundation targeting 128-bit provable security by the end of 2026.