Advanced Formal Verification of ZKP: How ZK Memory Was Proven

This post explains the formal verification of zkWasm's memory subsystem, detailing how dynamically sized state is represented via auxiliary tables (MTable/JTable), the alloc read/write abstraction that models mutable memory, and a counting scheme to prevent attacker-inserted table entries. It outlines the lemmas and inductive proofs used to show the tables correspond to intended memory operations, discusses a discovered bug in an earlier counting scheme, and argues for modular proof structure to scale verification across engineers.