Advanced Formal Verification of ZKP: A Tale of Two Bugs

This report examines zero-knowledge virtual machine (zkWasm) security, describing two representative ZK bugs: a Load8 coding error that allows higher bits to be uncontrolled and thus permits data injection, and a deeper design flaw where faked returns can be injected into execution tables to cause unauthorized state changes. It contrasts code bugs (shallow, fixable locally) with design bugs (deep, harder to detect), explains how auditing and formal verification (FV) detected the issues, and recommends combined auditing + FV and verifying both circuits and smart contracts to mitigate high-impact, hard-to-detect ZK vulnerabilities.