Verifying Compiler-Emitted WebAssembly in Lean

Proofs about generated code are usually stated at the source level, where an untrusted compiler still decides what runs. We instead prove properties of the compiled WebAssembly module itself. Such proofs are challenging because compiled modules can be large and require reasoning about low-level memory and control flow. We organize the proof so that the part a human must review is a short contract about values, while the machine-level obligations are delegated to coding agents and checked by Lean. We present \sysname, a Lean~4 framework that combines an executable small-step semantics with an iris-lean separation logic and reusable rules for compiler idioms. Its step function is proved equivalent to the relation the proofs use. It passes 99\% of the official conformance suite's records with no semantic failures, interpreter errors, or out-of-fuel results. Two Rust case studies illustrate the approach, both compiled at optimization level~3 against the standard library, an allocator, and host imports. For a binary GCD that reads and writes a byte stream, we prove that the module runs to completion without trapping and writes the greatest common divisor of its two inputs for every input pair, with no fuel bound; the contract a reviewer reads is six lines about the two words and their divisor. For an allocating merge sort of 56 linked functions, we prove that every finite terminal execution either writes a sorted permutation of the input or ends in a designated out-of-memory trap.